The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 04/05/2014 08:00 PM, Ömer Sinan Ağacan wrote:
> This eval command fails with stack overflow. It works fine when n is
> 8. I was wondering what am I doing wrong, in most other languages same
> function works for n > 500 without problems. Or is this because Coq's
> default stack depth is very low?
That is because you are using natural numbers in unary representation. 
Already something like:

  Check 362880.

results in

  Warning: Stack overflow or segmentation fault happens
  when working with large numbers in nat (observed
  threshold may vary from 5000 to 70000 depending on
  your system limits and on the command executed).

  Stack overflow.

Better use a more efficient representation for natural numbers like N 
(an inductive representation as bit sequences) or bigN (arbitrary 
precision machine integers).