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