[Agda] automatically instantiating rewrites

[Nils Anders Danielsson]

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.

-- 
/NAD