[Agda] [agda2] how to programming the basic

[Mandy Martino]

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/


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