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