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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
