diff options
| author | Vincent Semeria | 2019-08-28 00:21:26 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-09-16 19:00:23 +0200 |
| commit | beeb3ed57c4749ff84524250a8b79dfa0b1e2f78 (patch) | |
| tree | b05e00b39f3037b8c495185ce69976653a735b85 /doc/stdlib | |
| parent | 09953295ea86eaf78c6688a1a2861aa6f41cd9ab (diff) | |
Define morphisms of real numbers and accelerate Cauchy reals
Prove that morphisms preserve additions
Fix stdlib index
Prove that constructive real morphisms preserve multiplications by integers
Prove that constructive real morphisms preserve multiplications by rationals
Prove CReal_mult_pos_appart_zero
Prove that constructive real morphisms preserve multiplications
Prove that constructive real morphisms preserve divisions
Rewrite convergence in sort Prop, to extract smaller programs
Rewrite convergence on integers, to extract smaller programs
Fix typos
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index cc91776a4d..d1b98b94a3 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -515,7 +515,9 @@ through the <tt>Require Import</tt> command.</p> <dd> theories/Reals/Rdefinitions.v theories/Reals/ConstructiveReals.v + theories/Reals/ConstructiveRealsMorphisms.v theories/Reals/ConstructiveCauchyReals.v + theories/Reals/ConstructiveCauchyRealsMult.v theories/Reals/Raxioms.v theories/Reals/ConstructiveRIneq.v theories/Reals/ConstructiveRealsLUB.v |