Загрузка стандартной библиотеки Agda

Question

Я установил Agda (версия 2.3.2.2) и стандартную библиотеку (версия 0.7).
Я могу загрузить программу, которая не импортирует стандартную библиотеку.
Например, я могу загрузить

data Bool : Set where 
true : Bool 
false : Bool 

not : Bool -> Bool 
not false = true 
not true = false 

Однако, я не могу загрузить

open import Data.Bool 
data Bool : Set where 
true : Bool 
false : Bool 

not : Bool -> Bool 
not false = true 
not true = false 

Когда я загружаю стандартную библиотеку, я получил ниже ошибки.

/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 

Любые идеи для исправления ошибки?

Answer 1

Уверены ли вы в версиях? 2.3.2.2 должен быть совместим с 0,7. Мне кажется, что ваша Агда более поздняя, ​​чем 2.3.2.2. Есть файл ...\Agda-2.3.2.2\lib\prim\Agda\Primitive.agda? Этого не должно быть.

Если это не помогает, вы можете попробовать вручную изменить содержание Level модуля к следующему:

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 

Но вы, вероятно, сталкиваются с другими вопросами.

И вы действительно хотите, чтобы старые версии Agda и stdlib?