dest_vartype

Type.dest_vartype : hol_type -> string

Breaks a type variable down to its name.

Failure

Fails with dest_vartype if the type is not a type variable.

Example

> dest_vartype alpha;
val it = "'a": string

> try dest_vartype bool;
Exception- HOL_ERR (at Type.dest_vartype: not a type variable) raised

See also

Type.mk_vartype, Type.is_vartype, Type.dest_type