with type t = LogtkFOTerm.t * LogtkFOTerm.t
and type rhs = LogtkFOTerm.t
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 -> LogtkIndex.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.