<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body>
<div id="compose" contenteditable="true" style="padding-left: 20px; padding-right: 20px; padding-bottom: 8px;">
<div>I do not think that there is error.</div>
<div>Already defined zero2, but it return left expression error. I do not know what the wrong is.</div>
<div>
<div class="acompli_signature">Sent from <a href="https://aka.ms/sdimjr">Outlook Mobile</a></div>
<br>
</div>
</div>
<div class="gmail_quote">_____________________________<br>
From: Andreas Abel <<a href="mailto:abela@chalmers.se" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="1">abela@chalmers.se</a>><br>
Sent: Sunday, January 24, 2016 4:45 PM<br>
Subject: Re: [Agda] [agda2] how to programming the basic<br>
To: Mandy Martino <<a href="mailto:tesleft@hotmail.com" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="4">tesleft@hotmail.com</a>>, <<a href="mailto:mechvel@scico.botik.ru" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="5">mechvel@scico.botik.ru</a>><br>
Cc: <<a href="mailto:agda@lists.chalmers.se" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="6">agda@lists.chalmers.se</a>><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>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="9">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="10">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
<br>
<br>
</div>
</body>
</html>