The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

2014-04-05 21:31 GMT+03:00 Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>:
> 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).

Ah, that makes sense, thanks Robbert!

Any ideas about rest of my questions?

---
Ömer Sinan Ağacan
http://osa1.net