CODEWITHSUNDEEP
agda
Adjam
Adjam

Reputation: 640

Trying to compile basic program in Agda

I've got agda running on my machiene but I'm having difficulty running a basic example from the 'learn you an agda' tutorial

the web page is here: http://learnyouanagda.liamoc.net/pages/peano.html

I've put together the code from the tutorial

module peano where

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

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

but when I try 'loading' the file, in preperation for compiling it throws the following error:

/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

How do I get this code to compile and run? I don't know how to add a library like 'peano'. I'm an agda beginner and a really clear walk through with code examples would be much appreciated.

If I just do

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

The file compiles

If I just skip the peano library like this

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


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

then I get the error

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

How do I fix this? Do I need peano to make this code compile? If so how do I do that?

Upvotes: 1

Views: 631

Answers (1)

gallais
gallais

Reputation: 12103

To fix your first error, you need to carefully read the error message:

The name of the top level module does not match the file name.

Your file is called first_program.agda and not peano.agda hence the error. You need to either rename the file or call the toplevel module first_program.

Once the module header is removed, I don't get your second error: the file parses just fine for me.

Upvotes: 1

Related Questions