[Agda] [agda2] how to programming the basic

[Andreas Abel]

Well, you are defining _+2_, but the first clause is a rule for _*2_.

On 24.01.2016 11:27, 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 <https://aka.ms/sdimjr>
>
> _____________________________
> From: Andreas Abel <abela at chalmers.se <mailto: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 <mailto:tesleft at hotmail.com>>,
> <mechvel at scico.botik.ru <mailto:mechvel at scico.botik.ru>>
> Cc: <agda at lists.chalmers.se <mailto: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)
>
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se <mailto:andreas.abel at gu.se>
> http://www2.tcs.ifi.lmu.de/~abel/
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/