<div><div class="gmail_quote">On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton <span dir="ltr"><<a href="mailto:wren@freegeek.org">wren@freegeek.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 3/17/11 5:12 PM, Conor McBride wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 17 Mar 2011, at 18:35, wren ng thornton wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Another question on particulars. When dealing with natural numbers, we<br>
run into the problem of defining subtraction. There are a few<br>
reasonable definitions:<br>
</blockquote>
<br>
No there aren't.<br>
</blockquote>
<br></div>
How about "pragmatically efficacious"?<br></blockquote><div> </div><div>If you must, you could always fall back on an encoding similar to the one that Brent used when introducing virtual species:<div><br></div>
<div><a href="http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/">http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/</a></div><div><br></div><div>along with some setoid that normalized for comparison on them, or you could just switch to type level Integers.</div>
<div><br></div><div>-Edward<br></div></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
-- <br>
Live well,<br><font color="#888888">
~wren</font><div><div></div><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>