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 Kananaskis-14