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