[Agda] automatically instantiating rewrites

Nils Anders Danielsson nad at chalmers.se
Mon Jan 16 18:55:56 CET 2012

On 2012-01-14 19:54, Ramana Kumar wrote:
> Is there any plan to (or, more interestingly, never to) support this
> kind of rewriting that automatically picks a matching term?

As far as I know there are no immediate plans to provide this feature.
However, it may already be possible to implement such a feature /inside/
the language, using quoting; people more familiar with the reflection
machinery may know more.


More information about the Agda mailing list