[Agda] Inconsistent rewrite behavior

[Andreas Abel]

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/