Module Syntax.Rule

Exception raised when trying to create an invalid rewrite rule.

Abstract type for rule.

A TRS is a list of rule

rule_mk l r creates a rewriting rule with l as lhs and r as rhs.

• raises Invalid_rule

  if l and r satisfy one of the folowing conditions:

  • l is a variable term, i.e., x == Var _
  • there is a free variable in r that doesn't appear free in l

lhs r returns the lef-hand-side term of the rewrite rule r.

rhs r returns the right-hand-side term of the rewrite rule r.

equal r r' is whether r is structurally equal to r'. Two rules are equal if their respective lhs (rhs) terms are structurally equal (module alpha-equivalence).

to_string r returns a string representation of r.

get_label trs returns the string label of the trs trs.