1\DOC var_compare
2
3\TYPE {var_compare : term * term -> order}
4
5\SYNOPSIS
6Total ordering on variables.
7
8\KEYWORDS
9variable, order.
10
11\DESCRIBE
12An invocation {var_compare (v1,v2)} will return one of
13{{LESS, EQUAL, GREATER}}, according to an ordering on term
14variables. The ordering is transitive and total.
15
16\FAILURE
17If {v1} and {v2} are not both variables.
18
19\EXAMPLE
20{
21- var_compare (mk_var("x",bool), mk_var("x",bool --> bool));
22> val it = LESS : order
23}
24
25
26\COMMENTS
27Used to build high performance datastructures for dealing with sets
28having many variables.
29
30\SEEALSO
31Term.empty_varset, Term.compare.
32\ENDDOC
33