[Agda] A Demonstration of Agda by Alan Jeffrey

[Peter Hancock]

> data List# ( A : Set ) : ℕ → Set where
>    [] : List# A 0
>    _:::_ : ∀ { n } → A → List# A n → List# A (n ⊹ 1)

Try replacing the last line with

     _:::_ : ∀ { n } → A → List# A n → List# A (suc n)

I am not sure what Agda thinks "1" is, or whether (+1) is
definitionally equal to suc.  (The way you have defined it.
(1+) is definitionally equal to suc, I think.)


Basically, you have to learn how to interpret the error messages
Agda gives you, which gets easier but can still be hard.  Try to imagine what
is going on in type-checking, perhaps by doing it carefully on
paper.  The messages should begin to make more sense.
Constraints of definitional equality are being synthesised and checked.


All the best,
Peter Hancock