News for hackers. Stuff that matters.
Re:Now I’m calculating with constructive reals by simiones on Wednesday April 27, 2022 @07:06AM (#31178484)
I would note that the fact that 0.(9) = 1 can be talked about and shown using just the Rational numbers, you don't need to invoke the Reals.
Re:Now I’m calculating with constructive reals by peterhalburt33 on Wednesday April 27, 2022 @02:43PM (#31184071)
Completely correct. Too lazy to amend my answer, but even rational numbers don’t have a unique decimal representation.