[Agda] parse errors with the latest version

[Dominique Devriese]

Ondrej,

I think you should try to replace
  open import Relation.Binary.PropositionalEquality
with
  open import Relation.Binary.PropositionalEquality hiding ([_])

This [_] constructor is probably new in the latest release of the
standard library.

Dominique

Op 30 maart 2012 12:18 heeft Ondrej Rypacek <ondrej.rypacek at gmail.com>
het volgende geschreven:
> 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