----------------------------------------------------------------------
compare                                                         (Type)
----------------------------------------------------------------------
Type.compare : hol_type * hol_type -> order

SYNOPSIS
An ordering on HOL types.

KEYWORDS
ordering, type.

DESCRIBE
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
Term.compare.

----------------------------------------------------------------------