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
Am 16.03.2014 11:29, schrieb Henning Thielemann:
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:
http://hackage.haskell.org/package/base-4.7.0.0/candidate/
Am 16.03.2014 09:40, schrieb Christiaan Baaij:
To answer the second question (under the assumption that you want
phantom-type style Vectors and not GADT-style):
That works, someNatVal was the missing piece.
Now the natural next question is how to perform type-level induction on
Nat. This
