diff options
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 52 |
2 files changed, 43 insertions, 10 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 3af16cb731..0a9dba99a9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -91,3 +91,4 @@ theories/setoid_ring/Rings_Z.v theories/setoid_ring/ZArithRing.v theories/ssr/ssrunder.v theories/ssr/ssrsetoid.v +theories/ssrsearch/ssrsearch.vo diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4a62888552..ab615d5f65 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -21,6 +21,8 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Byte.v theories/Init/Nat.v theories/Init/Decimal.v + theories/Init/Hexadecimal.v + theories/Init/Numeral.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v @@ -235,7 +237,15 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/DecimalPos.v theories/Numbers/DecimalN.v theories/Numbers/DecimalZ.v + theories/Numbers/DecimalQ.v theories/Numbers/DecimalString.v + theories/Numbers/HexadecimalFacts.v + theories/Numbers/HexadecimalNat.v + theories/Numbers/HexadecimalPos.v + theories/Numbers/HexadecimalN.v + theories/Numbers/HexadecimalZ.v + theories/Numbers/HexadecimalQ.v + theories/Numbers/HexadecimalString.v </dd> <dt> <b> NatInt</b>: @@ -530,18 +540,15 @@ through the <tt>Require Import</tt> command.</p> Formalization of real numbers </dt> <dd> + <dl> + <dt> <b>Classical Reals</b>: + Real numbers with excluded middle, total order and least upper bounds + </dt> + <dd> theories/Reals/Rdefinitions.v - theories/Reals/Cauchy/ConstructiveCauchyReals.v - theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v - theories/Reals/Cauchy/ConstructiveCauchyAbs.v theories/Reals/ClassicalDedekindReals.v + theories/Reals/ClassicalConstructiveReals.v theories/Reals/Raxioms.v - theories/Reals/Abstract/ConstructiveReals.v - theories/Reals/Abstract/ConstructiveRealsMorphisms.v - theories/Reals/Abstract/ConstructiveLUB.v - theories/Reals/Abstract/ConstructiveAbs.v - theories/Reals/Abstract/ConstructiveLimits.v - theories/Reals/Abstract/ConstructiveSum.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -587,7 +594,6 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v - theories/Reals/Cauchy/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v @@ -607,6 +613,31 @@ through the <tt>Require Import</tt> command.</p> (theories/Reals/Reals.v) theories/Reals/Runcountable.v </dd> + <dt> <b>Abstract Constructive Reals</b>: + Interface of constructive reals, proof of equivalence of all implementations. EXPERIMENTAL + </dt> + <dd> + theories/Reals/Abstract/ConstructiveReals.v + theories/Reals/Abstract/ConstructiveRealsMorphisms.v + theories/Reals/Abstract/ConstructiveLUB.v + theories/Reals/Abstract/ConstructiveAbs.v + theories/Reals/Abstract/ConstructiveLimits.v + theories/Reals/Abstract/ConstructiveMinMax.v + theories/Reals/Abstract/ConstructivePower.v + theories/Reals/Abstract/ConstructiveSum.v + </dd> + <dt> <b>Constructive Cauchy Reals</b>: + Cauchy sequences of rational numbers, implementation of the interface. EXPERIMENTAL + </dt> + <dd> + theories/Reals/Cauchy/ConstructiveRcomplete.v + theories/Reals/Cauchy/ConstructiveCauchyReals.v + theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v + theories/Reals/Cauchy/ConstructiveCauchyAbs.v + </dd> + + </dl> + </dd> <dt> <b>Program</b>: Support for dependently-typed programming @@ -676,5 +707,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v + theories/Compat/Coq813.v </dd> </dl> |