[Agda] Parse error on standard library's Relation.Binary

[Andreas Abel]

Hi Jim,

I have tried your example, it works for me.  I am using Agda2 from the 
darcs repository.  Might be advisable, since things are still much in 
the flow.

Cheers,
Andreas

Jim Apple wrote:
> 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
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/