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

Question

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?

Answer 1

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.