7 Feb
2008
7 Feb
'08
7:15 p.m.
On Feb 7, 2008 8:38 PM, Dan Weston
I know that naming is arbitrary, but...
Digits in types seems ugly to me. In this case, it is also redundant. Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed, so confusion is even increased with Nat0.
Ok, fair enough. I changed the names of Positives and Naturals (which do include 0) for Pos and Nat. The change (together with a connective rename from :+ to :* ) is already pushed in the darcs repository.