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

Я установил 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

Есть идеи исправить ошибку?


installation standard-library agda
person mmsss    schedule 09.04.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы уверены в версиях? 2.3.2.2 должен быть совместим с 0.7. Мне кажется, ваша Agda более свежая, чем 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?

person user3237465    schedule 09.04.2016
comment
Версия Агды не была 2.3.2.2! Извините и спасибо! Я могу загрузить библиотеку! - person mmsss; 09.04.2016