Is there a function to extract a value from a Singleton?

Question

I'm developing a data type which requires an SNat, and would like to have the ability to give the user a Nat instead. Searching on Hoogle has yet to yield results.

That is, is there a function

f :: forall a (x :: a). Sing a x -> a

?

Answer 1

You can use fromSing from singletons