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