agdaagda-mode

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?

Solution

  • 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.