----------------------------------------------------------------------
var_compare                                                     (Term)
----------------------------------------------------------------------
var_compare : term * term -> order

SYNOPSIS
Total ordering on variables.

KEYWORDS
variable, order.

DESCRIBE
An invocation {var_compare (v1,v2)} will return one of
{{LESS, EQUAL, GREATER}}, according to an ordering on term
variables. The ordering is transitive and total.

FAILURE
If {v1} and {v2} are not both variables.

EXAMPLE

- var_compare (mk_var("x",bool), mk_var("x",bool --> bool));
> val it = LESS : order




COMMENTS
Used to build high performance datastructures for dealing with sets
having many variables.

SEEALSO
Term.empty_varset, Term.compare.

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