On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton
On 3/17/11 5:12 PM, Conor McBride wrote:
On 17 Mar 2011, at 18:35, wren ng thornton wrote:
Another question on particulars. When dealing with natural numbers, we run into the problem of defining subtraction. There are a few reasonable definitions:
No there aren't.
How about "pragmatically efficacious"?
If you must, you could always fall back on an encoding similar to the one that Brent used when introducing virtual species: http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/ along with some setoid that normalized for comparison on them, or you could just switch to type level Integers. -Edward
-- Live well, ~wren
_______________________________________________ Agda mailing list Agda@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda