<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&nbsp;</div>
<div><br>
</div>
<div>Do it have priority of defining which first?</div>
<div><br>
</div>
<div>Because &#43;2 and *2 &nbsp;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, &quot;Sergei Meshveliani&quot;
<span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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 &#43;0000, Mandy Martino wrote:<br>
&gt; I do not think that there is error.<br>
&gt; Already defined zero2, but it return left expression error. I do not<br>
&gt; know what the wrong is.<br>
&gt; Sent from Outlook Mobile<br>
&gt; <br>
<br>
&gt; _____________________________<br>
&gt; From: Andreas Abel &lt;abela@chalmers.se&gt;<br>
&gt; Sent: Sunday, January 24, 2016 4:45 PM<br>
&gt; Subject: Re: [Agda] [agda2] how to programming the basic<br>
&gt; To: Mandy Martino &lt;tesleft@hotmail.com&gt;, &lt;mechvel@scico.botik.ru&gt;<br>
&gt; Cc: &lt;agda@lists.chalmers.se&gt;<br>
&gt; <br>
&gt; <br>
&gt; &quot;What is wrong in this picture?&quot;<br>
&gt; <br>
&gt; &gt; _&#43;2_ : Nat2 -&gt; Nat2 -&gt; Nat2<br>
&gt; &gt; zero2 *2 m = zero2<br>
&gt; &gt; suc n &#43;2 m = suc (n &#43;2 m)<br>
&gt; <br>
<br>
1) Where _*2_&nbsp; is defined?<br>
&nbsp;&nbsp; It needs to be defined earlier.<br>
<br>
2) Probably you intend&nbsp; _&#43;2_&nbsp; to define addition of natural numbers.<br>
&nbsp;&nbsp; But this program does not define the value for&nbsp; (zero2 &#43;2 m).<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
&nbsp; <br>
<br>
<br>
<br>
<br>
</div>
</span></font>
</body>
</html>