[Agda] automatically instantiating rewrites

[Nils Anders Danielsson]

On 2012-01-12 19:34, Ramana Kumar wrote:
> If you have an equation of the form eqn : (x : t) → foo x ≡ bar x, is
> it possible to use rewrite in such a way that it picks up all
> instances of foo x and rewrites them, or do you always have to
> manually apply eqn to the right terms before you can give it to
> rewrite?

The latter. The rewrite construct is defined in terms of with:

   http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6

-- 
/NAD