[Agda] "Not in scope" error

[Robert Rothenberg]

On 02/07/08 19:32 Nils Anders Danielsson wrote:
> 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.

Ouch. What's the command to type that in? (There really should be an ASCII 
synonym for it.)

> 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).

How does one use case split? I can't get it to work.