[Agda] parse errors with the latest version

Dominique Devriese dominique.devriese at cs.kuleuven.be
Fri Mar 30 12:29:42 CEST 2012


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


More information about the Agda mailing list