module TRS:`SIG_TRS`

`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`

.