On 10/14/10 1:35 AM, Henning Thielemann wrote:
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
Not presently, but it is easy to implement such a function: reifyInt :: Int -> (forall n. NaturalNumber n => N n -> a) -> a reifyInt i f = case intToUnknownN i of UnknownN n -> f n Is this what you were thinking of? Cheers, Greg