[Agda] automatically instantiating rewrites

[Ramana Kumar]

Yes, I'd love to hear from anyone who knows how to get the
quoting/reflection machinery to do rewriting like this (or any other
interesting tactics).
I'll have a go myself.

On Mon, Jan 16, 2012 at 5:55 PM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20120117/ec37e1a4/attachment.html