coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CoqIde crash on Eval compute

From: Rui Baptista <rpgcbaptista AT gmail.com>
To: Marcus Ramos <mvmramos AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] CoqIde crash on Eval compute
Date: Sat, 31 Aug 2013 15:45:53 +0100

That is not a bug. Either the unary natural 43210 takes too much memory, or addition and multiplication on unary naturals that size require too much recursion. Hence the stack overflow. Use binary naturals instead.

[Coq-Club] CoqIde crash on Eval compute, Marcus Ramos, 08/30/2013
- Re: [Coq-Club] CoqIde crash on Eval compute, Rui Baptista, 08/31/2013
  - Re: [Coq-Club] CoqIde crash on Eval compute, Marcus Ramos, 08/31/2013
    - Re: [Coq-Club] CoqIde crash on Eval compute, Rui Baptista, 08/31/2013