[Agda] automatically instantiating rewrites

[Ramana Kumar]

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120112/86a50f95/attachment.html