[Agda] "Not in scope" error

[Nils Anders Danielsson]

On Wed, Jul 2, 2008 at 7:17 PM, Robert Rothenberg <robrwo at gmail.com> wrote:
>
> _·_ : {a : Set} -> [ Transposition a ] -> a -> a
> []        · z = z
> (t :: ts) · z = ts · (t ·' z)

The Data.List library uses ∷ (U+2237) for cons, not two colons. In
variable-width fonts these strings may be more or less
indistinguishable.

A hint: If you use case-split (C-c C-c), then Agda fills in the
patterns for you in a syntactically correct way (unless you stumble
upon some bug).

-- 
/NAD