[Agda] automatically instantiating rewrites

Nils Anders Danielsson nad at chalmers.se
Thu Jan 12 19:46:44 CET 2012

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:



More information about the Agda mailing list