type-level induction on Nat

[Richard Eisenberg]

On Mar 16, 2014, at 6:29 AM, Henning Thielemann wrote:

> 
> Since the unary natural number kind so ubiquituous in examples, is there a recommended module to import it from, which also contains the injectivity magic of FromNat1? I cannot see it in:
> 

No. After some debate (on the libraries list, perhaps?), we decided to remove this from `base`, and I don't know of another library that has taken it on. If it were possible just to define a *kind* Nat1 with *type-level* conversions to and from Nat, we would have kept it in. But, we had to define a *type* Nat1 as well, and it only seemed sensible to have all the class instances, etc., to use this type in terms. This led to a fair amount of code, none of which was tightly coupled to code in `base`.

There is a data-nat library, but it doesn't have the conversions to/from Nat built in.

Richard