Questions tagged [real-numbers]
For questions about $\mathbb{R}$, the field of real numbers.
2
questions
3
votes
2
answers
88
views
State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types
I don't think a particular choice of such type theory matters much.
Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types.
Reals is supposed to be a Set (in HoTT ...
- 173
14
votes
1
answer
213
views
Converting between formulations of reals in Coq
While trying to answer more concretely a question on floating points, I tried proving a simple statement using the Flocq library of Coq. However, I got stuck before really exercising it because I am ...
- 482