Re: Proving properties of type-level natural numbers obtained from user input

On 25 November 2014 at 19:34, Richard Eisenberg wrote:

If I were you, I would just write `g` using unsafeCoerce in the right spot, instead of bothering with all the singletons, which would have to use unsafety anyway.

Thanks, I hadn't considered this yet. Cheers, Bas