compare

Term.compare : term * term -> order

Ordering on terms.

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.

See also

Term.empty_tmset, Term.var_compare