CODEWITHSUNDEEP
agdaagda-mode
user65526
user65526

Reputation: 705

Loading files in Agda: unclear explanation in Learn you an Agda

I have made an emacs file trial_agda.agda with the following code:

module trial_agda where

data π•Ÿ : Set where
  zero : π•Ÿ
  suc  : π•Ÿ β†’ π•Ÿ

data _even : π•Ÿ β†’ Set where
  ZERO : zero even
  STEP : βˆ€ x β†’ x even β†’ suc (suc x) even

_+_ : π•Ÿ β†’ π•Ÿ β†’ π•Ÿ
(zero + n) = n
(suc n) + nβ€² = suc (n + nβ€²)

In http://learnyouanagda.liamoc.net/pages/proofs.html, the author writes:

Now we’ll prove in Agda that four is even. Type the following into an emacs buffer, and type C-c C-l:

-- \_1 to type ₁
proof₁ : suc (suc (suc (suc zero))) even
proof₁ = ?

I typed C-c C-n and then copied and pasted the above code. I received the error Error: First load the file.

What has gone wrong?

Upvotes: 1

Views: 165

Answers (1)

user65526
user65526

Reputation: 705

It is required to add the code to the same emacs file, underneath the code defining the module and the types, etc.

This was not specified in the book.

Upvotes: 1

Related Questions