在 Agda 中加载文件：Learn you an Agda 中的解释不清楚

Question

我用以下代码制作了一个 emacs 文件 trial_agda.agda：

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′)

在http://learnyouanagda.liamoc.net/pages/proofs.html中，作者写道：

现在我们将在 Agda 中证明四是偶数。在 emacs 缓冲区中键入以下内容，然后键入 C-c C-l:

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

我输入了C-c C-n，然后复制并粘贴了上面的代码。我收到错误 Error: First load the file.

出了什么问题？

Answer 1

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

这在书中没有说明。