mathlib

d749b205 - feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575)

feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575) This isn't all that useful, but it gives a slightly nicer experience for users who are surprised when `#eval (2 + 3 : real)` emits a gigantic pile of garbage.