dest_type : hol_type -> string * hol_type list
STRUCTURE
SYNOPSIS
Breaks apart a non-variable type.
DESCRIPTION
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", [`:'a`, `:bool`]) : string * hol_type list

COMMENTS
A more precise alternative is dest_thy_type, which tells which theory the type operator was declared in.
SEEALSO
HOL  Kananaskis-10