1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
\DOC dest_type
\TYPE {dest_type : hol_type -> string * hol_type list}
\SYNOPSIS
Breaks apart a type (other than a variable type).
\DESCRIBE
{dest_type(`:(ty1,...,tyn)op`)} returns {("op",[`:ty1`;...;`:tyn`])}.
\FAILURE
Fails with {dest_type} if the type is a type variable.
\EXAMPLE
{
# dest_type `:bool`;;
val it : string * hol_type list = ("bool", [])
# dest_type `:(bool)list`;;
val it : string * hol_type list = ("list", [`:bool`])
# dest_type `:num -> bool`;;
val it : string * hol_type list = ("fun", [`:num`; `:bool`])
}
\SEEALSO
mk_type, dest_vartype.
\ENDDOC
|
