The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

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.

Yes, most functions of Coq (the type-checker, the printer, and most
auxiliary functions) are simply recursive. Rewriting all of them
tail-recursively would increase the complexity of the code for a
limited benefice since after all most use of large numbers is for
computation and binary numbers are for this purpose much more
efficient.

Your situation is maybe an exception. If you don't compute at all with
1114112, a possibility is to leave it as a parameter of your
development or to write 

     Require Import Nnat.
     Definition N1114112 := nat_of_N 1114112.
     Definition unicode_codepoint (n:nat) : Prop :=
         n < N1114112.

without never evaluating the constant (1114112 is now in N and hence
in binary representation).

Otherwise, if you do have computations involving 1114112, I would
indeed recommend using N rather than nat.

Best regards,

Hugo Herbelin