Gwern Branwen wrote:

I've actually long wondered about this: why don't more functions use Nat where it'd make sense? It can't be because Nat is hard to define - I'd swear I've seen many definitions of Nat (if not dozens when you count all the type-level exercises which include one).

Because naive definitions are dog-slow and fast definitions are anything but easy to use?