[Haskell-cafe] ANNOUNCE: type-level-natural-number and friends!

[Henning Thielemann]

Gregory Crosswhite schrieb:

> === natural-number v1.0 ===
> 
> This package provides *value*-level natural numbers that are tagged with
> a type-level natural number corresponding to their value by using GADTs,
> as well as some simple operations on them.  I also provide an instance
> for the EqT class in type-equality, which means that you can compare two
> natural numbers with possibly different tags and obtain a proof of
> equality if and only if they are the same type.  The extensions that are
> required to use this package are  Rank2Types and GADTs.  (The package
> itself only uses GADTs, but it pulls in
> type-level-natural-number-induction which uses Rank2Types.)

Is there also a 'reify' function, that allows to convert an Int or Peano
value locally to a type level number?

reifyInteger :: Integer -> (forall n. Nat n => n -> a) -> a