blob: 182f8a805c73a3b8c2a8e378dc9ea56521413eb4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
- **Added:**
Module `Reals.ConstructiveCauchyReals` defines constructive real numbers
by Cauchy sequences of rational numbers
(`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
with the help and review of Guillaume Melquiond and Bas Spitters).
- **Changed:** Classical real numbers are now defined
as a quotient of these constructive real numbers, which significantly reduces
the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`),
while preserving backward compatibility.
Futhermore, the new axioms for classical real numbers include the limited
principle of omniscience (`sig_forall_dec`), which is a logical principle
instead of an *ad hoc* property of the real numbers.
(`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
with the help and review of Guillaume Melquiond and Bas Spitters)
|
