English
Real numbers can be realized as equivalence classes of Cauchy sequences of rationals; printing uses a chosen representative.
Русский
Действительные числа реализованы как эквивалентные классы по Коши последовательностей рациональных чисел; печать использует выбранного представителя.
LaTeX
$$$\mathbb{R} \cong \operatorname{CauSeq.Completion}(\mathbb{Q})$$$
Lean4
/-- Show an underlying Cauchy sequence for real numbers.
The representative chosen is the one passed in the VM to `Quot.mk`, so two Cauchy sequences
converging to the same number may be printed differently.
-/
unsafe instance : Repr ℝ where reprPrec r p := Repr.addAppParen ("Real.ofCauchy " ++ repr r.cauchy) p
