[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