[Agda] wierd error

[Ulf Norell]

On Thu, Jan 28, 2010 at 12:36 PM, Ruben Henner Zilibowitz <
rzilibowitz at yahoo.com.au> wrote:

> Hi,
>
> If I do that I get a parse error:
>
> WierdError.agda:12,15:
> Parse error )<ERROR> ≡⟨ refl ⟩ ( + m ) ≡⟨ x≡y ⟩ ....
>

Ah, the problem is that you've used the wrong kind of bar. The ascii bar is
reserved for the with construct, the abs function uses U+2223 which you get
by typing \| or \mid in the Agda input method.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100128/2146ab74/attachment.html