[Agda] [agda2] how to programming the basic

[Sergei Meshveliani]

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