从Agda文档复制代码编译报错：Nat不在作用域中

错误原因 #

Agda标准库中，Nat（自然数类型）和suc（后继函数）并非默认全局可用，它们定义在Data.Nat模块内，直接使用会触发“不在作用域”的报错。

解决方法 #

你需要显式导入Data.Nat模块，以下两种方式均可：

方式1：基础导入 #

在代码开头添加导入语句，直接使用Nat和suc：

module hello-world where

open import Data.Nat

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

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

方式2：带public选项导入 #

如果希望子模块也能直接使用这些名字，添加public选项后，导入的名字会自动开放给当前模块的子模块：

module hello-world where

open import Data.Nat public

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

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

验证步骤 #

1. 保存修改后的代码
2. 在Emacs中按下Ctrl+c Ctrl+l重新编译，报错即可消除

内容的提问来源于stack exchange，提问作者Werner Germán Busch