module E: Index_intf.EQUATION
Module that describes indexed equations
type
t
type
rhs
An equation can have something other than a term as a right-hand
side, for instance a formula.
val compare : t -> t -> int
Total order on equations
: t -> Index_intf.term * rhs * bool
Obtain a representation of the (in)equation. The sign indicates
whether it is an equation l = r
(if true) or an inequation
l != r
(if false)
val priority : t -> int
How "useful" this equation is. Can be safely ignored by
always returning the same number.