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

[Andreas Abel]

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 = {!!}

This works, so there might be indeed a problem with Agda.  However, I  
am not an expert on the rewrite feature...

Maybe you can continue with the hand-translated code instead...

Cheers,
Andreas

On Oct 2, 2010, at 9:29 AM, David Leduc wrote:

>
>
> open import Relation.Binary.PropositionalEquality
>
> test : (A : Set)(u v : A)(p q : u ≡ v) -> A
> test A u v p q rewrite p | sym q = {!!}

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/