Module Rule


module Rule: sig .. end

Rewrite rules definitions




The variables of the rhs must be included in the lhs

type rule = private
| Mk of Term.term * Term.term
val mk : Term.term * Term.term -> rule
val compare : rule -> rule -> int
Comparison and equality up to lhs-variables renaming
val eq : rule -> rule -> bool
val fprintf : rule Useful.fprintf
Print an equation
module OrdRul: ORD_PRT  with type t = rule
module RulSet: Myset.S  with type elt = rule
val symbols_of_rule : rule -> Symb.SymbolSet.t
Symbols of a set of rules
val symbols_of_rules : RulSet.t -> Symb.SymbolSet.t