diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
| commit | d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 (patch) | |
| tree | 575ec66b8028a599f94d293ae32260b09e7874ef /doc/stdlib | |
| parent | 1dccdb6b2c792969c5e09faebc2f761e46192ec4 (diff) | |
Numbers : log2. Abstraction, properties and implementations.
Btw, we finally declare the original Zpower as the power on Z.
We should switch to a more efficient one someday, but in the
meantime BigN is proved with respect to the old one.
TODO: reform Zlogarithm with respect to Zlog_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4f208c7da..e0f445d03 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -183,6 +183,7 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zpow_def.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v + theories/ZArith/Zlog_def.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v @@ -238,6 +239,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZProperties.v theories/Numbers/NatInt/NZPow.v theories/Numbers/NatInt/NZSqrt.v + theories/Numbers/NatInt/NZLog.v </dd> </dt> @@ -281,6 +283,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NParity.v theories/Numbers/Natural/Abstract/NPow.v theories/Numbers/Natural/Abstract/NSqrt.v + theories/Numbers/Natural/Abstract/NLog.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v |