diff options
| author | Pierre-Marie Pédrot | 2019-12-02 11:04:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-02 11:04:25 +0100 |
| commit | 003512ecebae24bd518155f5a92b851a8f9bcd08 (patch) | |
| tree | 363a665d195b109d9c76004196f67566a178b4a1 /doc/changelog/10-standard-library/10827-dedekind-reals.rst | |
| parent | 31e109671896ef42653b1fcf239d8ebe1424c3da (diff) | |
| parent | 71e80467cbdec4472360876043ad885eca347207 (diff) | |
Merge PR #11031: Release notes 8.11
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). |