[Haskell-cafe] [Agda] Defining subtraction for naturals
ekmett at gmail.com
Fri Mar 18 00:06:37 CET 2011
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:
along with some setoid that normalized for comparison on them, or you could
just switch to type level Integers.
> Live well,
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe