The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi,

The following definition results in a stack overflow from coqc:

    Definition unicode_codepoint (n:nat) : Prop :=
        n < 1114112.

Presumably some code is trying to process 1 million nested S(...) 
constructors and isn't tail-recursive.

I've replaced it with this definition, using the N type instead of nat, 
that seems to work:

    Definition unicode_codepoint (n:N) : Prop :=
        Ncompare n (1114112%N) = Lt.

Is it impossible to manipulate numbers of reasonable size using nat? Is 
it recommended to use N instead?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com