[Agda] "Not in scope" error
Robert Rothenberg
robrwo at gmail.com
Wed Jul 2 16:50:10 CEST 2008
I have the following:
data Transposition (a : Set) : Set where
?_,_? : a -> a -> Transposition a
_·'_ : Transposition a -> a -> a
? x , y ? ·' z = if (z == x) then y
else if (z == y) then x
else z
_·_ : [ Transposition a ] -> a -> a
[] · z = z
(t::?) · z = ? · (t ·' z)
which gives me the error:
Not in scope:
?
This doesn't make sense to me. t::? is of type [ Transposition a ] and ?
should therefore be the tail (and also of type [ Transposition a ].
More information about the Agda
mailing list