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 | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst deleted file mode 100644 index 11efef4de0..0000000000 --- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **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 - Dedekind reals, hidden behind an opaque module. - Classical Dedekind reals are a quotient of constructive reals, which allows - to transport many constructive proofs to the classical case. - - (`#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). |