Module Order


module Order: sig .. end

Term ordering utilities




type ord =
| Greater
| Equal
| Smaller
| Uncomparable
Result type for comparison functions
type 'a cmp = 'a -> 'a -> ord 
val partition : 'a cmp ->
('a * 'a) list ->
('a * 'a) list * ('a * 'a) list * ('a * 'a) list * ('a * 'a) list
Partition a list of pairs into those whose lhs is greater, equal, etc. than the rhs
val int_of_ord : ord -> int
val opp : ord -> ord
val comp : ord cmp
val ge : ord -> bool
val le : ord -> bool
val lex : 'a cmp -> 'a list cmp
Lexicographic extension of an ordering
exception IncompletePrecedence of Symb.symbol * Symb.symbol
exception IncompatibleStatus of Symb.symbol * Symb.symbol
val rpo_fail : Parsetree.rpo_status Symb.SymbolMap.t ->
Symb.symbol cmp -> Term.term cmp
val rpo : Parsetree.rpo_status Symb.SymbolMap.t ->
Symb.symbol cmp -> Term.term cmp
Recursive Path Ordering