Proposal: Add inductively-defined Nat to base

[Henning Thielemann]

On Fri, 6 Apr 2018, Jon Purdy wrote:

> One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first
> learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second
> constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a
> lazy “Nat” (and “Ord” instance I guess).

It would also work with:
    void xs > replicate 1 ()