coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 2048

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: AUGER Cédric <sedrikov AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] 2048
Date: Sun, 30 Mar 2014 17:43:56 +0200

On 03/30/2014 06:08 PM, AUGER Cédric wrote:

Le Sun, 30 Mar 2014 01:14:35 +0100,
Laurent Théry
<Laurent.Thery AT inria.fr>
a écrit :

For a small increase in performances, it would have been better to
remember only the exponent, instead of the whole natural number (unary
integers are not very good wrt Coq memory when they can become quite
big).

Thanks! I have updated the file using N instead of nat .

http://www-sop.inria.fr/marelle/Laurent.Thery/T2048.v

--
Laurent

[Coq-Club] 2048, Laurent Théry, 03/30/2014
- Re: [Coq-Club] 2048, Kevin Sullivan, 03/30/2014
- Re: [Coq-Club] 2048, Matthieu Sozeau, 03/30/2014
- Re: [Coq-Club] 2048, AUGER Cédric, 03/30/2014
  - Re: [Coq-Club] 2048, Pierre-Yves Strub, 03/30/2014
    - Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
  - Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
    - Re: [Coq-Club] 2048, Gabriel Scherer, 03/30/2014