时间戳

首页 > 解决方案 > 尝试在 Agda 中编译基本程序

agda - 尝试在 Agda 中编译基本程序

问题描述

我在我的机器上运行了 agda，但我在运行“学习 agda”教程中的基本示例时遇到了困难

网页在这里： http: //learnyouanagda.liamoc.net/pages/peano.html

我已经把教程中的代码放在一起

module peano where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ 
zero + zero = zero
zero + n    = n
(suc n) + n′ = suc (n + n′)

但是当我尝试“加载”文件时，在准备编译它时会引发以下错误：

/home/adjam/Desktop/first_program.agda:3,8-13
The name of the top level module does not match the file name. The
module peano should be defined in one of the following files:
  /home/adjam/Desktop/peano.agda
  /home/adjam/Desktop/peano.lagda
  /usr/share/agda-stdlib/peano.agda

如何让这段代码编译和运行？我不知道如何添加像“peano”这样的库。我是一个 agda 初学者，非常感谢您通过代码示例进行非常清晰的演练。

如果我只是这样做

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

文件编译

如果我像这样跳过 peano 库

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ


_+_ : ℕ → ℕ → ℕ 
zero + zero = zero
zero + n    = n
(suc n) + n′ = suc (n + n′)

然后我得到错误

/home/adjam/Desktop/first_program.agda:10,1-1
/home/adjam/Desktop/first_program.agda:10,1: Parse error
_+_<ERROR>
 : ℕ → ℕ → ℕ 
zero + zero = ze...

我该如何解决？我需要 peano 来编译这段代码吗？如果是这样，我该怎么做？

标签： agda

解决方案

要修复您的第一个错误，您需要仔细阅读错误消息：

顶级模块的名称与文件名不匹配。

您的文件被调用first_program.agda，因此不会peano.agda出现错误。您需要重命名文件或调用顶层模块first_program。

删除模块标头后，我不会收到您的第二个错误：该文件对我来说解析得很好。

推荐阅读