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.