[Agda] Defining subtraction for naturals

[Nils Anders Danielsson]

On 2011-03-17 19:35, wren ng thornton wrote:
> Dependently typed languages tend to use the second definition because it
> gives a pure total function (unlike the first) and because it's less
> obnoxious to use than the third. In Haskell the third would be even more
> obnoxious.

There is a fourth option: a comparison view. See "The view from the
left" by Conor McBride and James McKinna (Section 6).

(This option is similar to what Henning Thielemann suggested.)

-- 
/NAD