1\DOC dest_type
2
3\TYPE {dest_type : hol_type -> string * hol_type list}
4
5\SYNOPSIS
6Breaks apart a non-variable type.
7
8\DESCRIBE
9If {ty} is a type constant, then {dest_type ty} returns {(ty,[])}.
10If {ty} is a compound type {(ty1,...,tyn)tyop}, then {dest_type ty}
11returns {(tyop,[ty1,...,tyn])}.
12
13\FAILURE
14Fails if {ty} is a type variable.
15
16\EXAMPLE
17{
18- dest_type bool;
19> val it = ("bool", []) : string * hol_type list
20
21- dest_type (alpha --> bool);
22> val it = ("fun", [`:'a`, `:bool`]) : string * hol_type list
23}
24
25
26\COMMENTS
27A more precise alternative is {dest_thy_type}, which tells which theory
28the type operator was declared in.
29
30\SEEALSO
31Type.mk_type, Type.dest_thy_type, Type.dest_vartype.
32\ENDDOC
33