[Agda] Defining subtraction for naturals

[gallais at EnsL.org]

I would be glad if you could say which definition of « m - n » is the
one that you see as the reasonable one (and why it is the case).

In my opinion, the reasonable definition is the one that uses the
exception monad because:
- m - n is not in |N when m < n (so we failed at computing it)
- returning zero when m < n is morally an exception handling (this
should come on top of the computation and not pollute it)
- giving a proof that n < m should not be mandatory because this
condition is decidable (a soundness lemma seems a better option to me)

But I am maybe missing something?

Cheers,
--
guillaume



On 17 March 2011 22:12, Conor McBride <conor at strictlypositive.org> 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.
>
> Conor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>