compare
Type.compare : hol_type * hol_type -> order
An ordering on HOL types.
An invocation compare (ty1,ty2) returns one of
{LESS, EQUAL, GREATER}. This is a total and transitive order.
Failure
Never fails.
Example
> Type.compare (bool, alpha --> alpha);
val it = LESS: order
Comments
One use of compare is to build efficient set or dictionary
datastructures involving HOL types in the keys.
There is also a Term.compare.