[Agda] This must be a type checking bug, right?
David Leduc
david.leduc6 at googlemail.com
Sat Oct 2 09:29:06 CEST 2010
The simple code below fails type checking with the error message
Failed to infer the value of dotted pattern
when checking that the pattern ._ has type A
However if I replace "sym q" by "sym p", then it type checks!
How can I convince Agda that it is well typed?
module test where
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 = {!!}
More information about the Agda
mailing list