aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Cauchy
AgeCommit message (Collapse)Author
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
Add real numbers up to 10
2020-05-03Simplify division of Cauchy realsVincent Semeria
Improve comments
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
Force Cauchy modulus equal to identity, make division transparent Fix test
2020-04-29Reduce rational numbers in Cauchy real addition, to accelerate itVincent Semeria
2020-04-22Document Cauchy realsVincent Semeria
2020-04-19Use binary integers for Cauchy realsVincent Semeria
2020-04-18Make multiplication of Cauchy reals transparent and accelerate itVincent Semeria
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:54:57 +0000