[Agda] "Not in scope" error

[Robert Rothenberg]

On 02/07/08 19:06 Nils Anders Danielsson wrote:
> On Wed, Jul 2, 2008 at 5:47 PM, Robert Rothenberg <robrwo at gmail.com> wrote:
>> However, I still get the error
> 
> Can you send a complete example exhibiting the problem?
> 

-------------- next part --------------
open import Relation.Binary
open import Data.Bool
open import Data.List

module Labels {a : Set} (_==_ : a -> a -> Bool) where

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

_·_ : {a : Set} -> [ Transposition a ] -> a -> a
[]        · z = z
(t :: ts) · z = ts · (t ·' z)