<div dir="ltr"><div>Just to get the example running, you could make it a postulate. Then you don't have to bother providing a proof.<br><br></div>postulate<br><div><div> plus-commute : (a b : Nat) → a + b ≡ b + a</div>
<div><br>
</div><br></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Fri, Feb 5, 2016 at 8:05 PM, Mandy Martino <span dir="ltr"><<a href="mailto:tesleft@hotmail.com" target="_blank">tesleft@hotmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div 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" title="http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite
Ctrl+Click or tap to follow the link" target="_blank">http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite</a></p>
<div style="margin-bottom:20px;overflow:auto;width:100%;text-indent:0px">
<table style="width:90%;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)" cellspacing="0">
<tbody>
<tr style="border-spacing:0px" valign="top">
<td colspan="2" style="vertical-align:top;padding:0px;display:table-cell">
<div></div>
<div style="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 href="http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite" style="text-decoration:none" target="_blank">With-Abstraction — Agda 2.5 documentation</a></div>
<div 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">
<a href="http://agda.readthedocs.org" target="_blank">agda.readthedocs.org</a></div>
<div 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>
<div>Regards,</div>
<div><br>
</div>
<div>Martin </div>
</div>
</div>
</div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>