[Agda] parse errors with the latest version

Ondrej Rypacek ondrej.rypacek at gmail.com
Fri Mar 30 12:18:37 CEST 2012


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


More information about the Agda mailing list