尝试用Agda编写basic程序

Question

我已经在我的机器上运行了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来编译这段代码吗？如果是这样，我该怎么做呢？

Answer 1

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

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

您的文件名为first_program.agda，而不是peano.agda，因此出现错误。您需要重命名该文件或调用toplevel模块first_program。

一旦删除了模块头，我就看不到您的第二个错误了:文件对我来说可以很好地解析。