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兼容。在我看来，你们的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的旧版本吗？