[Agda] Inconsistent rewrite behavior

[Martin Stone Davis]

Reported here: https://github.com/agda/agda/issues/1692

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com

On Sun, Oct 18, 2015 at 10:54 AM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> On 18.10.2015 09:34, Martin Stone Davis wrote:
>
>> I've noticed inconsistent behavior in the rewrite mechanism. An exemplar
>> is shown here <http://lpaste.net/143252>, where I've been making
>> revisions to Data.AVL. See my comments in the last function, lemjl-.
>> When I rewrite v₂ ≡ v₁ and check the context of a goal, I find that one
>> of the variables of interest has been rewritten but another has not. Is
>> this expected behavior?
>>
>
> I can confirm this behavior, but I would not say it is expected.  Can you
> shrink this example (to something not requiring the standard library) and
> report an issue?
>
> Cheers,
> Andreas
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151018/992a2c6f/attachment.html