[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