dest_thy_type

Type.dest_thy_type
    : hol_type -> {Thy:string, Tyop:string,
                   Args:hol_type list}

Breaks apart a type (other than a variable type).

If ty is an application of a type operator Tyop, which was declared in theory Thy, to a list of types Args, then dest_thy_type ty returns {Tyop,Thy,Args}.

Failure

Fails if ty is a type variable.

Example

> dest_thy_type “:'a -> bool”;
val it = {Args = [“:α”, “:bool”], Thy = "min", Tyop = "fun"}:
   {Args: hol_type list, Thy: string, Tyop: string}

> try dest_thy_type alpha;
Exception- HOL_ERR at Type.dest_thy_type: raised

See also

Type.mk_thy_type, Type.dest_type, Type.mk_type, Term.mk_thy_const