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>