Попытка скомпилировать базовую программу в Агде - PullRequest
0 голосов
/ 21 марта 2019

У меня agda работает на моем компьютере, но у меня возникают трудности с запуском базового примера из учебника "Learn you a 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». Я новичок в агде, и я очень благодарен за действительно понятный обзор примеров кода.

Если я просто сделаю

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 для компиляции этого кода? Если да, то как мне это сделать?

1 Ответ

1 голос
/ 21 марта 2019

Чтобы исправить вашу первую ошибку, вам необходимо внимательно прочитать сообщение об ошибке:

Имя модуля верхнего уровня не соответствует имени файла.

Ваш файл называется first_program.agda, а не peano.agda, следовательно, ошибка. Вам нужно либо переименовать файл, либо вызвать модуль верхнего уровня first_program.

Как только заголовок модуля удален, я не получаю вашу вторую ошибку: файл разбирается просто отлично.

...