CODEWITHSUNDEEP
installationstandard-libraryagda
mmsss
mmsss

Reputation: 273

Loading Standard Library of Agda

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

Answers (1)

effectfully
effectfully

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

Related Questions