Module Equation


module Equation: sig .. end

Equations for completion




type eqn = private
| Mk of Term.term * Term.term
val mk : Term.term * Term.term -> eqn
val compare : eqn -> eqn -> int
Equality up to renaming of variables
val eq : eqn -> eqn -> bool
val fprintf : eqn Useful.fprintf
Print an equation into a formatter
module OrdEqn: ORD_PRT  with type t = eqn
module EqnSet: Myset.S  with type elt = eqn
val add_non_trivial_pair : (Term.term -> Term.term) ->
Term.term * Term.term -> EqnSet.t -> EqnSet.t
val add_non_trivial : (Term.term -> Term.term) ->
eqn -> EqnSet.t -> EqnSet.t
val remove_trivial : (Term.term -> Term.term) -> EqnSet.t -> EqnSet.t
val is_commutativity : eqn -> bool
Test if an equation is the commutativity equation
val has_commutativity : EqnSet.t -> bool
val remove_commutativity : EqnSet.t -> EqnSet.t
val partition : Term.term Order.cmp ->
EqnSet.t ->
EqnSet.t * EqnSet.t * EqnSet.t
Partition a set of equations into those whose lhs is greater, smaller or something else