[Agda] "Not in scope" error

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Wed Jul 2 17:18:13 CEST 2008


On Wed, Jul 2, 2008 at 3:50 PM, Robert Rothenberg <robrwo at gmail.com> wrote:

> _·_ : [ Transposition a ] -> a -> a
> []     · z = z
> (t::?) · z = ? · (t ·' z)

>  Not in scope:
>  ?

Agda requires whitespace around operators:

  (t :: ?) · z = ? · (t ·' z)

(I assume that you did not really use a question mark, since this
would have led to another error.)

-- 
/NAD


More information about the Agda mailing list