加载 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 的旧版本吗？