[Agda] [agda2] how to programming the basic

[Mandy Martino]

I use the script in tutorial and just append 2

Do it have priority of defining which first?

Because +2 and *2  depend on each other

I guess the original script in tutorial do not have this problem.

Sent from Outlook Mobile<https://aka.ms/sdimjr>




On Sun, Jan 24, 2016 at 4:28 AM -0800, "Sergei Meshveliani" <mechvel at botik.ru<mailto:mechvel at botik.ru>> wrote:

On Sun, 2016-01-24 at 10:27 +0000, Mandy Martino wrote:
> I do not think that there is error.
> Already defined zero2, but it return left expression error. I do not
> know what the wrong is.
> Sent from Outlook Mobile
>

> _____________________________
> From: Andreas Abel <abela at chalmers.se>
> Sent: Sunday, January 24, 2016 4:45 PM
> Subject: Re: [Agda] [agda2] how to programming the basic
> To: Mandy Martino <tesleft at hotmail.com>, <mechvel at scico.botik.ru>
> Cc: <agda at lists.chalmers.se>
>
>
> "What is wrong in this picture?"
>
> > _+2_ : Nat2 -> Nat2 -> Nat2
> > zero2 *2 m = zero2
> > suc n +2 m = suc (n +2 m)
>

1) Where _*2_  is defined?
   It needs to be defined earlier.

2) Probably you intend  _+2_  to define addition of natural numbers.
   But this program does not define the value for  (zero2 +2 m).

Regards,

------
Sergei






-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160124/a7510a6e/attachment.html