Thanks to Jean-Philippe Bernardy for idea and implementation!<div><br></div><div>From the release notes:</div><div><br></div><div><div>* New rewrite construct</div><div><br></div><div> If eqn : a ≡ b, where _≡_ is the builtin equality (specified with a BUILTIN EQUALITY pragma)</div>
<div> you can now write</div><div><br></div><div> f ps rewrite eqn = rhs</div><div><br></div><div> for</div><div><br></div><div> f ps with a | eqn</div><div> ... | ._ | refl = rhs</div><div><br></div><div> The rewrite construct has the effect of rewriting the goal and the</div>
<div> context by the given equation (left to right).</div><div><br></div><div> You can rewrite by several equations (in sequence) by separating them</div><div> by bars:</div><div><br></div><div> f ps rewrite eqn₁ | eqn₂ | .. = rhs</div>
<div><br></div><div> It is also possible to add with clauses after rewriting:</div><div><br></div><div> f ps rewrite eqns with e</div><div> ... | p = rhs</div><div><br></div><div> Note that pattern matching happens before rewriting--if you want to rewrite</div>
<div> and then do pattern matching you can use a with after the rewrite.</div><div><br></div><div> See <a href="http://code.haskell.org/Agda/test/succeed/Rewrite.agda">http://code.haskell.org/Agda/test/succeed/Rewrite.agda</a> for some example uses.</div>
<div><br></div><div>/ Ulf</div></div>