dest_type
Type.dest_type : hol_type -> string * hol_type list
Breaks apart a non-variable type.
If ty is a type constant, then dest_type ty returns (ty,[]). If
ty is a compound type (ty1,...,tyn)tyop, then dest_type ty returns
(tyop,[ty1,...,tyn]).
Failure
Fails if ty is a type variable.
Example
> dest_type bool;
val it = ("bool", []): string * hol_type list
> dest_type (alpha --> bool);
val it = ("fun", [“:α”, “:bool”]): string * hol_type list
Comments
A more precise alternative is dest_thy_type, which tells which theory
the type operator was declared in.