加载 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 吗？

加载 Agda 的标准库

Loading Standard Library of Agda

installation

standard-library

agda