Module type LogtkRewriting.SIG_TRS

module type SIG_TRS = sig .. end

type t 
type rule = LogtkFOTerm.t * LogtkFOTerm.t 
rewrite rule, from left to right
val empty : unit -> t
val add : t ->
rule -> t
val add_seq : t ->
rule Sequence.t -> t
val add_list : t ->
rule list -> t
val to_seq : t -> rule Sequence.t
val of_seq : rule Sequence.t -> t
val of_list : rule list -> t
val size : t -> int
val iter : t -> (rule -> unit) -> unit
val rule_to_form : rule -> LogtkFormula.FO.t
Make a formula out of a rule (an equality)
val rewrite_collect : t ->
LogtkFOTerm.t -> LogtkFOTerm.t * rule list
Compute normal form of the term, and also return the list of rules that were used.
val rewrite : t -> LogtkFOTerm.t -> LogtkFOTerm.t
Compute normal form of the term. See LogtkRewriting.SIG_TRS.rewrite_collect.