diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-17 21:00:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-17 21:00:24 +0000 |
| commit | b1040ad095410fe925b0a3aaf9399776279486f0 (patch) | |
| tree | 53f791ef62a4d15d553ba9785e174facb32063c7 /theories/NArith | |
| parent | 5297477d29c7e80ce1a6a2cb9d0fc61fcee3a651 (diff) | |
Nicer log2 function for nat (suggested by Hugo)
The auxiliary variable q is now increased continuously instead
of being doubled from time to time. Interest: this version is
obviously linear, and specification proofs are slightly simplier.
NB: the previous version was in fact also linear I think, but
proving this requires a proper complexity analysis.
I'm sure this algorithm is related with some cellular automata
stuff in the spirit of the firing squad :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13720 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith')
0 files changed, 0 insertions, 0 deletions