coq/theories/Reals/Cauchy, branch master The formal proof system Remove some trivial definition. 2021-02-19T18:39:38+00:00 Guillaume Melquiond 2021-02-19T18:37:50+00:00 fccbde39ff8085f73bdb46dac278f88474a1e202 






Abstract the non-computational part away.
2021-02-19T18:29:46+00:00

Guillaume Melquiond

2021-02-19T18:29:46+00:00

21ed2bfa901108d69893bc8480d215edeb255d6d












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.







CReal: changed epsilon for modulus of convergence from 1/n to 2^z
2020-06-09T08:19:17+00:00

Michael Soegtrop

2020-05-02T13:14:12+00:00

3d775bdd6094912ebc3801c1dad3bbdd5863b315












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







Simplify division of Cauchy reals
2020-05-03T09:13:15+00:00

Vincent Semeria

2020-05-02T16:25:13+00:00

dc3e3577afcaeaa7e13c13307074eb99a30b3982

Improve comments





Improve comments







Replace QSeqEquiv by QCauchySeq, simplify proofs.
2020-04-30T21:21:29+00:00

Vincent Semeria

2020-04-30T16:27:21+00:00

18544983e1b2a342c8bbcbd3c51003b11453213f

Force Cauchy modulus equal to identity, make division transparent

Fix test





Force Cauchy modulus equal to identity, make division transparent

Fix test







Reduce rational numbers in Cauchy real addition, to accelerate it
2020-04-29T16:28:07+00:00

Vincent Semeria

2020-04-29T16:28:07+00:00

c4a24b7a7844789a08dabe8a76b20c239a8b8218












Document Cauchy reals
2020-04-22T17:41:20+00:00

Vincent Semeria

2020-04-22T17:41:20+00:00

a4432d05514a60f59b7917331abfb9f589d8ca85