Real numbers from Cauchy sequences #
This file defines
ℝ as the type of equivalence classes of Cauchy sequences of rational numbers.
This choice is motivated by how easy it is to prove that
ℝ is a commutative ring, by simply
lifting everything to
Extra instances to short-circuit type class resolution.
These short-circuits have an additional property of ensuring that a computable path is found; if
Field ℝ is found first, then decaying it to these typeclasses would result in a
version of them.
The real numbers are a
*-ring, with the trivial
0 is the default value for
Real.sSup of the empty set or sets which are not bounded above, it
suffices to show that all elements of
S are bounded by a nonnegative number to show that
is bounded by this number.