[Agda] A Demonstration of Agda by Alan Jeffrey

[mukesh tiwari]

Hi Peter
Thank you!


On Sun, Mar 24, 2013 at 3:22 PM, Peter Hancock <hancock at spamcop.net> wrote:

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

I will keep this in mind.


>
>
> All the best,
> Peter Hancock
>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130324/afbd8fb3/attachment.html