Agda 中缺少类型签名错误，我不知道如何避免

Question

我在 emacs 的文件 trial_agda.agda 中有以下代码：

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#fn1 中，没有提到在讨论这个例子的地方应该有这样的差距。