instReprCauchy — Mathlib

English

There is an implementation of Repr for CauSeq.Completion.Cauchy that prints a finite preview of a representative sequence.

Русский

Существует реализация Repr для CauSeq.Completion.Cauchy, печатающая конечный фрагмент образца последовательности.

LaTeX

$$Repr (CauSeq.Completion.Cauchy abv)$$

Lean4

/-- Show the first 10 items of a representative of this equivalence class of Cauchy sequences.

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 β] : Repr (Cauchy abv) where
  reprPrec r
    _ :=
    let N := 10
    let seq := r.unquot
    "(sorry /- " ++ Std.Format.joinSep ((List.range N).map <| repr ∘ seq) ", " ++ ", ... -/)"

Похожие утверждения