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

[Bas van Dijk]

On 25 November 2014 at 19:34, Richard Eisenberg <eir at cis.upenn.edu> 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