diff options
Diffstat (limited to 'doc/changelog/10-standard-library/10827-dedekind-reals.rst')
| -rw-r--r-- | doc/changelog/10-standard-library/10827-dedekind-reals.rst | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst index 5d8467025b..11efef4de0 100644 --- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -1,4 +1,5 @@ -- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers +- **Added:** + New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers as boolean-values functions along with 3 logical axioms: limited principle of omniscience, excluded middle of negations and functional extensionality. The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those @@ -6,6 +7,6 @@ Classical Dedekind reals are a quotient of constructive reals, which allows to transport many constructive proofs to the classical case. - See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, + (`#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, - code review by Hugo Herbelin. + code review by Hugo Herbelin). |