Term.compare : term * term -> order
STRUCTURE
SYNOPSIS
Ordering on terms.
DESCRIPTION
An invocation compare (M,N) will return one of {LESS, EQUAL, GREATER}, according to an ordering on terms. The ordering is transitive and total, and equates alpha-convertible terms.
FAILURE
Never fails.
EXAMPLE
- compare (T,F);
> val it = GREATER : order

- compare (Term `\x y. x /\ y`, Term `\y z. y /\ z`);
> val it = EQUAL : order

COMMENTS
Used to build high performance datastructures for dealing with sets having many terms.
SEEALSO
HOL  Trindemossen-1