<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Exchange Server">
<!-- converted from text --><style><!-- .EmailQuote { margin-left: 1pt; padding-left: 4pt; border-left: #800000 2px solid; } --></style>
</head>
<body>
<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>
</body>
</html>