var_compare : term * term -> order
STRUCTURE
SYNOPSIS
Total ordering on variables.
DESCRIPTION
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
HOL  Kananaskis-10