[Agda] Defining subtraction for naturals

[wren ng thornton]

On 3/17/11 2:50 PM, Luke Palmer wrote:
> If you are implementing lazy naturals, I wonder if defining 0 - 1 to
> be infinity makes mathematical sense.  It's like arithmetic mod
> infinity....

Actually, I'm specifically implementing strict naturals :)

There are a number of libraries for lazy naturals out there already, but 
for my current project I need the efficiency of Int/Integer--- without 
the errors or defensive programming that comes from using them when we 
mean Nat/Natural.

So far I haven't actually needed arithmetic operations (Enum, Eq, and 
Ord have been enough) but I figure I should square that away before 
splitting the code off for a public release. Since the whole thing is 
done as newtypes I can always make the Num instances the "right" ones, 
since people who obsess over performance can manually unwrap them to 
perform raw operations they know/hope will succeed and then revalidate 
the invariants when they're done with the arithmetic section. I just 
want to make sure the instance I give has the nice mathematical 
properties it could/should.

-- 
Live well,
~wren