Agda 错误：从文档编译示例时不在范围内

Question

我有以下 Agda 文件（名为 hello-world.agda），直接取自 Agda 文档：

module hello-world where

  module B where
    f : Nat → Nat
    f n = suc n

  g : Nat → Nat → Nat
  g n m = m

但是当我执行 Ctrl c、Ctrl l 时，我在 emacs 上收到以下错误：

Not in scope:
  Nat at C:\Users\myname\Documents\Agda\hello-world.agda:4,9-12
when scope checking Nat

Answer 1

文档中的示例不完整，它只是为了展示模块系统的基础知识（尽管我确实认为尽可能使示例自包含会很好）。

这是进行类型检查的一种方法，假设您已经安装了

agda-stdlib

，您可能会这样做：

module hello-world where

  open import Data.Nat renaming (ℕ to Nat)

  module B where
    f : Nat → Nat
    f n = suc n

  g : Nat → Nat → Nat
  g n m = m

或者你可以更换

  open import Data.Nat renaming (ℕ to Nat)

与

  data Nat : Set where
    zero : Nat
    suc : Nat -> Nat

另请注意，Agda 文档在这里稍微误导了您，通常顶层模块的内容不会缩进，即大多数时候人们会这样写

module hello-world where

open import Data.Nat renaming (ℕ to Nat)

module B where
  f : Nat → Nat
  f n = suc n

g : Nat → Nat → Nat
g n m = m

相反。并不是说它太重要，只是节省一些水平空间。