[Haskell-cafe] [Agda] Defining subtraction for naturals

[Edward Kmett]

On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton <wren at freegeek.org> wrote:

> 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 at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110317/02b98e35/attachment.htm>