A _rewrite rule_ has the form
Lab : l -> r where s
where =Lab= is the label or name of the rule, =l= is the left-hand side term pattern, =r= the right-hand side term pattern and =s= a strategy used as condition.
The application of a rule =Lab= to a term =t= consists of matching the left-hand side =l= to =t=,
applying the condition =s=, and then building the right-hand side =r=. On matching =l= the variables in =l= become bound. These variable bindings are used in the condition and the instantiation of the right-hand side.
Rules are implemented by translating them to more basic constructs. That is, a rule
Lab : l -> r where s
is translated to a StrategyDefinition
Lab = {x1,...,xn: ?l; where(s); !r}
See also
* [[Transformation Rule]]
* [[Contextual Rule]]
* [[Strategy Rule]]
* [[Anonymous Rewrite Rule]]
* [[Dynamic Rule]]
-- Main.EelcoVisser - 08 Jan 2002
------
CategoryGlossary