A missing type signature error in Agda which I do not know how to avoid

1
votes

I have the following code in a file trial_agda.agda in emacs:

module trial_agda where

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

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

It produces

/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

What is the problem?

1
agdaagda-mode

1 Answers

1
votes

The problem was resolved by making a gap of a line after suc: 𝕟 → 𝕟. In http://learnyouanagda.liamoc.net/pages/peano.html#fn1 where this example is mentioned, it is not mentioned where the example is discussed, that such a gap should be made.