converting data-level natural numbers to type-level

[Richard Eisenberg]

On Mar 15, 2014, at 4:48 PM, Henning Thielemann wrote:

> What is the meaning of KnownNat?

It is a Nat whose value is known at runtime. I'll confess to suggesting the name… I think I was hoping there would be more debate and a better idea at the time, but it just stuck.

I see that there is no good way to extract a KnownNat constraint from a singleton Nat. This is an oversight, and I'll be releasing a new version of singletons in the next week with this oversight fixed.

If you have other things you want from singletons, now is a good time to ask!

Thanks,
Richard