Reputation: 273
I installed Agda (version 2.3.2.2) and Standard Library (version 0.7).
I can load the program which doesn't import Standard Library.
For example, I can load
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not false = true
not true = false
However, I can not load
open import Data.Bool
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not false = true
not true = false
When I load Standard Library, I got below error.
/Users/my_name/.cabal/share/Agda-2.3.2.2/lib-0.7/src/Level.agda:27,1-32
Duplicate binding for built-in thing LEVEL, previous binding to.Agda.Primitive.Level
when checking the pragma BUILTIN LEVEL Level
Any ideas to fix the error?
Upvotes: 2
Views: 606
Reputation: 12735
Are you sure about the versions? 2.3.2.2 should be compatible with 0.7. It looks to me like your Agda is more recent than 2.3.2.2. Is there the ...\Agda-2.3.2.2\lib\prim\Agda\Primitive.agda
file? It shouldn't be there.
If that doesn't help, you can try to manually change the content of the Level
module to this:
module Level where
-- Levels.
open import Agda.Primitive public
using (Level; _⊔_)
renaming (lzero to zero; lsuc to suc)
-- Lifting.
record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
constructor lift
field lower : A
open Lift public
But you'll likely encounter other issues.
And do you really want that old versions of Agda and stdlib?
Upvotes: 2