14 Oct
2010
14 Oct
'10
2:07 p.m.
Gregory Crosswhite schrieb:
On 10/14/10 1:35 AM, Henning Thielemann wrote:
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?
I don't find the string "Unknown" in any of the three type-level-natural* packages.