Ошибка отсутствующей подписи типа в Agda, которую я не знаю, как избежать

Question

У меня есть следующий код в файле trial_agda.agda в emacs:

module trial_agda where

data  : Set where
 zero : 
 suc  :  → 
 _+_ :  →  → 

zero + n = n
(suc n) + n′ = suc (n + n′) 

Он производит

/Users/myname/trial_agda.agda:8,1-13
Missing type signature for left hand side zero + n
when scope checking the declaration
  zero + n = n

В чем проблема?

Answer 1

Проблема была решена путём разрыва строки после suc: → . В http://learnyouanagda.liamoc.net/pages/peano.html, где упоминается этот пример, не упоминается, где обсуждается пример, что следует сделать такой пробел.