coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Marcus Ramos <mvmramos AT gmail.com>
To: Rui Baptista <rpgcbaptista AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] CoqIde crash on Eval compute
Date: Mon, 2 Sep 2013 22:05:13 -0300

I didn´t realize that. Thank you.

2013/8/31 Rui Baptista <rpgcbaptista AT gmail.com>

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.

Re: [Coq-Club] CoqIde crash on Eval compute, Marcus Ramos, 09/03/2013