Я создал файл 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.
Что пошло не так?