<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;background-color:#FFFFFF;font-family:Calibri,Arial,Helvetica,sans-serif;">
<p>Hi ,</p>
<p><br>
</p>
<p><span style="font-size: 12pt;">when run the code directly, it return missing definition, </span></p>
<p><span style="font-size: 12pt;">how to write this definition?</span></p>
<p><span style="font-size: 12pt;"><br>
</span></p>
<p><span style="font-size: 12pt;">bb.agda:26,1-13</span><br>
</p>
<p></p>
<div>Missing definition for plus-commute</div>
<div><br>
</div>
<p></p>
<p>Following</p>
<p><a href="http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite" id="LPlnk999410" title="http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite
Ctrl+Click or tap to follow the link">http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite</a></p>
<div id="LPBorder_GT_14547314352780.9723990657366812" style="margin-bottom: 20px; overflow: auto; width: 100%; text-indent: 0px;">
<table id="LPContainer_14547314352710.2358145951293409" cellspacing="0" style="width: 90%; position: relative; overflow: auto; padding-top: 20px; padding-bottom: 20px; margin-top: 20px; border-top-width: 1px; border-top-style: dotted; border-top-color: rgb(200, 200, 200); border-bottom-width: 1px; border-bottom-style: dotted; border-bottom-color: rgb(200, 200, 200); background-color: rgb(255, 255, 255);">
<tbody>
<tr valign="top" style="border-spacing: 0px;">
<td id="TextCell_14547314352740.12015648023225367" colspan="2" style="vertical-align: top; position: relative; padding: 0px; display: table-cell;">
<div id="LPRemovePreviewContainer_14547314352740.5561670504976064"></div>
<div id="LPTitle_14547314352740.7005409994162619" style="top: 0px; color: rgb(33, 33, 33); font-weight: normal; font-size: 21px; font-family: wf_segoe-ui_light, 'Segoe UI Light', 'Segoe WP Light', 'Segoe UI', 'Segoe WP', Tahoma, Arial, sans-serif; line-height: 21px;">
<a id="LPUrlAnchor_14547314352750.13643565448001027" href="http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite" target="_blank" style="text-decoration: none;">With-Abstraction — Agda 2.5 documentation</a></div>
<div id="LPMetadata_14547314352760.18581023253500462" style="margin: 10px 0px 16px; color: rgb(102, 102, 102); font-weight: normal; font-family: wf_segoe-ui_normal, 'Segoe UI', 'Segoe WP', Tahoma, Arial, sans-serif; font-size: 14px; line-height: 14px;">
agda.readthedocs.org</div>
<div id="LPDescription_14547314352770.40905219432897866" style="display: block; color: rgb(102, 102, 102); font-weight: normal; font-family: wf_segoe-ui_normal, 'Segoe UI', 'Segoe WP', Tahoma, Arial, sans-serif; font-size: 14px; line-height: 20px; max-height: 100px; overflow: hidden;">
The clause containing the with-abstraction has no right-hand side. Instead it is followed by a number of clauses with an extra argument on the left, separated from ...</div>
</td>
</tr>
</tbody>
</table>
</div>
<br>
<div>open import Prelude</div>
<div><br>
</div>
<div>data Bool2 : Set where</div>
<div> true : Bool2</div>
<div> false : Bool2</div>
<div><br>
</div>
<div>not2 : Bool2 -> Bool2</div>
<div>not2 true = false</div>
<div>not2 false = true</div>
<div><br>
</div>
<div>identity2 : (A : Set) -> A -> A</div>
<div>identity2 A x = x</div>
<div><br>
</div>
<div>data Nat2 : Set where</div>
<div> zero2 : Nat2</div>
<div> suc : Nat2 -> Nat2</div>
<div><br>
</div>
<div>_or2_ : Bool2 -> Bool2 -> Bool2</div>
<div>false or2 x = x</div>
<div>true or2 _ = true</div>
<div><br>
</div>
<div>if2_then2_else2_ : (A : Set) -> Bool2 -> A -> A -> A</div>
<div>if2 true then2 x else2 y = x</div>
<div>if2 false then2 x else2 y = y</div>
<div><br>
</div>
<div>plus-commute : (a b : Nat) → a + b ≡ b + a</div>
<div><br>
</div>
<div>thm : (a b : Nat) → P (a + b) → P (b + a)</div>
<div>thm a b t with a + b | plus-commute a b</div>
<div>thm a b t | .(b + a) | refl = t</div>
<div><br>
</div>
<div>main = </div>
<div> if2_then2_else2_ Bool2 true (putStrLn "it is true") (putStrLn "it is else case")</div>
<div> putStrLn "Hello World"</div>
<br>
<p></p>
<p><br>
</p>
<div id="Signature">
<div>Regards,</div>
<div><br>
</div>
<div>Martin </div>
</div>
</div>
</body>
</html>