Module TopDown.S.Rewriting

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