module LogtkHORewriting:`sig`

..`end`

type`term =`

`LogtkHOTerm.t`

type`rule =`

`term * term`

`exception IllFormedRule of ``rule`

`type `

t

rewrite system

`val empty : ``t`

No rules

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

Add a rule. A rule must satisfy several conditions:

**Raises**

- every free variable on the RHS must occur in the LHS
- every free variable on the RHS must not occur under any binder (would cause problems with De Bruijn indices)

`IllFormedRule`

if the rule isn't valid.`val merge : ``t -> t -> t`

Merge two rewrite systems

module Seq:`sig`

..`end`

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

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

`include LogtkInterfaces.PRINT`

`include LogtkInterfaces.ORD`

`include LogtkInterfaces.HASH`

`val normalize : ``t -> term -> term`

Normalize the term w.r.t to the rewrite system

`val normalize_collect : ``t ->`

term -> term * rule list

Normalize the term, and returns a list of rules used to normalize it.