dest_type : hol_type -> string * hol_type list
- SYNOPSIS
-
Breaks apart a type (other than a variable type).
- DESCRIPTION
-
dest_type(`:(ty1,...,tyn)op`) returns ("op",[`:ty1`;...;`:tyn`]).
- FAILURE CONDITIONS
-
Fails with dest_type if the type is a type variable.
- EXAMPLE
-
# dest_type `:bool`;;
val it : string * hol_type list = ("bool", [])
# dest_type `:(bool)list`;;
val it : string * hol_type list = ("list", [`:bool`])
# dest_type `:num -> bool`;;
val it : string * hol_type list = ("fun", [`:num`; `:bool`])
- SEE ALSO
-
mk_type, dest_vartype.