[Agda] This must be a type checking bug, right?

[Jean-Philippe Bernardy]

On Sat, Oct 2, 2010 at 5:52 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi David,
>
> According to the 2.2.6 release notes,
>
>  http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6
>
> the rewrite in your function is translated as
>
> test' : (A : Set)(u v : A)(p q : u ≡ v) -> A
> test' A u v p q with u | p | v | sym p
> test' A u v p q | ._ | refl | ._ | refl = {!!}

The rewrite produces a cascade of with instead of them
being simultaneous, like you have written. That might explain the discrepancy.

Cheers,
-- JP