[Agda] A Demonstration of Agda by Alan Jeffrey

Peter Hancock hancock at spamcop.net
Sun Mar 24 10:52:15 CET 2013

> 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

More information about the Agda mailing list