Search code examples
agdaagda-mode

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

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?

Solution

  • 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.