[Agda] "Not in scope" error

[Robert Rothenberg]

On 02/07/08 16:18 Nils Anders Danielsson wrote:
> 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)

My mistake, due to misreading the Data.List file (which seems to omit the
space following the ::)

However, I still get the error (using "ts" instead of "\pi" for the question
mark):

  Could not parse the left-hand side (t :: ts) · z
  when scope checking the left-hand side (t :: ts) · z in the
  definition of _·_

I'm at a loss as what to do here.

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

It was a \pi symbol.