Загрузка файлов в 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 автор пишет:

Сейчас мы докажем в Агде, что четыре - это ровно. Введите следующее в буфер emacs и введите Cc Cl:

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

Я набрал C-c C-nа затем скопировал и вставил приведенный выше код. Я получил ошибкуError: First load the file.

Что пошло не так?

Answer 1

Требуется добавить код в тот же файл emacs под кодом, определяющим модуль, типы и т. Д.

В книге этого не указано.