module Rewriting:`sig`

..`end`

type`rule =`

`TopDown.S.T.t * TopDown.S.T.t`

`type `

t

A rewriting system. It is basically a mutable set of rewrite rules.

`val create : ``unit -> t`

New rewriting system

`val copy : ``t -> t`

Copy the rewriting system

`val add : ``t -> rule -> unit`

Add a rule to the system

`val add_list : ``t -> rule list -> unit`

`val to_list : ``t -> rule list`

List of rules

`val rewrite_root : ``t -> TopDown.S.T.t -> TopDown.S.T.t`

rewrite the term, but only its root. Subterms are not rewritten
at all.

`val rewrite : ``t -> TopDown.S.T.t -> TopDown.S.T.t`

Normalize the term recursively. The returned type cannot be rewritten
any further, assuming the rewriting system is **terminating**