[Agda] wierd error

[Ulf Norell]

On Thu, Jan 28, 2010 at 10:33 AM, Ruben Henner Zilibowitz <
rzilibowitz at yahoo.com.au> wrote:

> Hi,
>
> I am getting what seems like a wierd error that I can't debug. If someone
> could take a look and help fix this it would be quite instructive. Thanks.
> I'm using agda 2.2.6 with lib-0.2.
>
> WierdError.agda:11,43-12,10
> Could not parse the application begin + ∣ + m
> when scope checking begin + ∣ + m
>

Looks like an operator precedence issue. It should go through if you put
brackets around (+ ∣ + m ∣) and friends.

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