Загрузка файлов в Agda: непонятное объяснение в Learn You a 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, под кодом, определяющим модуль, типы и т. Д.

Это не было указано в книге.