[Agda] New rewrite construct

[Ulf Norell]

Thanks to Jean-Philippe Bernardy for idea and implementation!
>From the release notes:

* New rewrite construct

  If eqn : a ≡ b, where _≡_ is the builtin equality (specified with a
BUILTIN EQUALITY pragma)
  you can now write

    f ps rewrite eqn = rhs

  for

    f ps with a | eqn
    ... | ._ | refl = rhs

  The rewrite construct has the effect of rewriting the goal and the
  context by the given equation (left to right).

  You can rewrite by several equations (in sequence) by separating them
  by bars:

    f ps rewrite eqn₁ | eqn₂ | .. = rhs

  It is also possible to add with clauses after rewriting:

    f ps rewrite eqns with e
    ... | p = rhs

  Note that pattern matching happens before rewriting--if you want to
rewrite
  and then do pattern matching you can use a with after the rewrite.

  See http://code.haskell.org/Agda/test/succeed/Rewrite.agda for some
example uses.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091014/0294fcc6/attachment.html