coq/theories/Reals/Abstract, branch master The formal proof system Terminate some lemmas with Qed. 2021-02-19T15:28:35+00:00 Guillaume Melquiond 2021-02-19T15:13:45+00:00 b45ffd0bc0904e3d3325724e99b94239f5153b64 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. 
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.
Prove that classical reals implement constructive reals. Also move sums, min and max to CoRN. 2020-05-16T13:27:27+00:00 Vincent Semeria 2020-05-10T08:53:56+00:00 e663b606a3895b7c78ee528a94a5c6a9675683ca Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental 
Update stdlib index

Remove ConstructiveSum from the index

Add changelog entry

Make constructive reals experimental
Define CRzero and CRone via CR_of_Q 2020-05-09T15:43:06+00:00 Vincent Semeria 2020-05-09T08:09:51+00:00 598e24a9c4a81ec9f24f1088d0a7a4a93dc19fd4 Add real numbers up to 10 
Add real numbers up to 10
Missing apartness notations 2020-03-30T16:13:37+00:00 Vincent Semeria 2020-03-30T16:13:37+00:00 ea0bfc872a1363b47bf91e65fba0ecb770b39981 






Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files.
2020-03-27T17:30:38+00:00

Vincent Semeria

2020-03-01T16:30:57+00:00

ad91d136b8d51e859ce3b959674757818e753bcb

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





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