[Agda] parse errors with the latest version

[Dan Rosén]

Hi,

Relation.Binary.PropositionalEquality exports [_] since library version
0.6. See
http://www.cse.chalmers.se/~nad/listings/lib-0.6/Relation.Binary.PropositionalEquality.html#4005

One solution is to import this module hiding [_]:

open import Relation.Binary.PropositionalEquality hiding ([_])

Cheers,
Dan

(Sorry for double post - sent this from the wrong mail account)

On Fri, Mar 30, 2012 at 12:18 PM, Ondrej Rypacek
<ondrej.rypacek at gmail.com>wrote:

> Hi
>
> I've downloaded version 2.3.0 of agda , an .6 libraries, and some of
> my files have stopped parsing. Namely, I'm getting:
>
> Don't know how to parse C [ a , b ]. Could mean any one of:
>  C [ a , b ]
>  C ([ (a , b) ])
> when scope checking C [ a , b ]
>
>
> where _[_,_] is defined as a data constructor
>
>
> My imports are:
>
>
> open import Data.Nat
> open import Relation.Binary.PropositionalEquality
>
>
>
> I suspect this is a well known or trivial issue , so I'm not attaching
> the whole source code.
>
> Does anyone have an idea, what could be wrong?
>
> Cheers,
> Ondrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120330/69380184/attachment.html