<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Exchange Server">
<style>
<!--
.EmailQuote
{margin-left:1pt;
padding-left:4pt;
border-left:#800000 2px solid}
-->
</style>
</head>
<body>
<div>I understand now that it is the typing error * should be +</div>
<div><br>
</div>
<div>Thank you very much.<br>
<br>
<div class="acompli_signature">Sent from <a href="https://aka.ms/sdimjr">Outlook Mobile</a></div>
<br>
</div>
<br>
<br>
<br>
<div class="gmail_quote">On Sun, Jan 24, 2016 at 4:52 AM -0800, "Mandy Martino" <span dir="ltr">
<<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>></span> wrote:<br>
<br>
</div>
<div>
<div>
<div>I use the script in tutorial and just append 2 </div>
<div><br>
</div>
<div>Do it have priority of defining which first?</div>
<div><br>
</div>
<div>Because +2 and *2 depend on each other</div>
<div><br>
</div>
<div>I guess the original script in tutorial do not have this problem.<br>
<br>
<div class="x_acompli_signature">Sent from <a href="https://aka.ms/sdimjr">Outlook Mobile</a></div>
<br>
</div>
<br>
<br>
<br>
<div class="x_gmail_quote">On Sun, Jan 24, 2016 at 4:28 AM -0800, "Sergei Meshveliani"
<span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<br>
</div>
</div>
<font size="2"><span style="font-size:10pt">
<div class="PlainText">On Sun, 2016-01-24 at 10:27 +0000, Mandy Martino wrote:<br>
> I do not think that there is error.<br>
> Already defined zero2, but it return left expression error. I do not<br>
> know what the wrong is.<br>
> Sent from Outlook Mobile<br>
> <br>
<br>
> _____________________________<br>
> From: Andreas Abel <abela@chalmers.se><br>
> Sent: Sunday, January 24, 2016 4:45 PM<br>
> Subject: Re: [Agda] [agda2] how to programming the basic<br>
> To: Mandy Martino <tesleft@hotmail.com>, <mechvel@scico.botik.ru><br>
> Cc: <agda@lists.chalmers.se><br>
> <br>
> <br>
> "What is wrong in this picture?"<br>
> <br>
> > _+2_ : Nat2 -> Nat2 -> Nat2<br>
> > zero2 *2 m = zero2<br>
> > suc n +2 m = suc (n +2 m)<br>
> <br>
<br>
1) Where _*2_ is defined?<br>
It needs to be defined earlier.<br>
<br>
2) Probably you intend _+2_ to define addition of natural numbers.<br>
But this program does not define the value for (zero2 +2 m).<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
<br>
<br>
</div>
</span></font></div>
</body>
</html>