[Agda] Parse error on standard library's Relation.Binary
Jim Apple
jbapple+agda at gmail.com
Sun Dec 30 03:04:41 CET 2007
When attempting to compile
-----------------------------------
module Rank where
open import Data.Bool
-----------------------------------
$ agda --version
Agda 2 version 2.1.2
$ agda -i ~/pls/agda/lib RankMatching.agda
Checking Data.Bool ( /home/apple/pls/agda/lib/Data/Bool.agda )
Skipping Logic ( /home/apple/pls/agda/lib/Logic.agdai )
Skipping Data.Function ( /home/apple/pls/agda/lib/Data/Function.agdai )
Skipping Relation.Nullary ( /home/apple/pls/agda/lib/Relation/Nullary.agdai )
Checking Relation.Binary ( /home/apple/pls/agda/lib/Relation/Binary.agda )
/home/apple/pls/agda/lib/Relation/Binary.agda:27,5-5
/home/apple/pls/agda/lib/Relation/Binary.agda:27,5: Parse error
isEquivalence<ERROR> : IsEquivalence _≈_ refl ...
I downloaded the standard library today.
Any ideas?
Jim
More information about the Agda
mailing list