[Agda] wierd error

[Ruben Henner Zilibowitz]

Hi,

If I do that I get a parse error:

WierdError.agda:12,15:
Parse error )<ERROR> ≡⟨ refl ⟩ ( + m ) ≡⟨ x≡y ⟩ ...

Ruben

On 28/01/2010, at 9:44 PM, Ulf Norell wrote:

> 
> 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/e30439c0/attachment.html