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.