Type.compare : hol_type * hol_type -> order
STRUCTURE
Type
SYNOPSIS
An ordering on HOL types.
DESCRIPTION
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.

SEEALSO
compare
HOL  Kananaskis-14