[Agda] automatically instantiating rewrites

[Ramana Kumar]

Is there any plan to (or, more interestingly, never to) support this kind
of rewriting that automatically picks a matching term?
A middle ground could be to allow the interactive interface to provide a
list of probably matches.
I'm asking because I just wrote some long rewrite terms by hand by copying
from my goal the appropriate arguments to a general rule...

On Thu, Jan 12, 2012 at 6:46 PM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> 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:
>
>  http://wiki.portal.chalmers.**se/agda/agda.php?n=Main.**Version-2-2-6<http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6>
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20120114/48746ee7/attachment.html