[Agda] Inconsistent rewrite behavior

[Andreas Abel]

Thanks!

On 18.10.2015 22:46, Martin Stone Davis wrote:
> 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 <tel:3106993578>
> Electronic Mail: martin.stone.davis at gmail.com
> <mailto:martin.stone.davis at gmail.com>
> Website: martinstonedavis.com <http://martinstonedavis.com/>
>
> On Sun, Oct 18, 2015 at 10:54 AM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto: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 <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>
>


-- 
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/