[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