agda - 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?

标签： agdaagda-mode

Answer 1

需要将代码添加到同一个 emacs 文件中，在定义模块和类型等的代码下方。

这在书中没有具体说明。