Skip to content

Commit

Permalink
fix: unremove Repr (Cauchy abv) (#1524)
Browse files Browse the repository at this point in the history
This unremoves a working instance from mathlib3

Partially reverts e839638
  • Loading branch information
eric-wieser committed Jan 13, 2023
1 parent fb6c6c4 commit d04acbd
Showing 1 changed file with 10 additions and 11 deletions.
21 changes: 10 additions & 11 deletions Mathlib/Data/Real/CauSeqCompletion.lean
Expand Up @@ -279,17 +279,16 @@ theorem ofRat_div (x y : β) : ofRat (x / y) = (ofRat x / ofRat y : Cauchy abv)
simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]
#align cau_seq.completion.of_rat_div CauSeq.Completion.ofRat_div

-- Porting note: removed
-- /-- 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) ", " ++ ", ... -/)"
/-- 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) ", " ++ ", ... -/)"

end

Expand Down

0 comments on commit d04acbd

Please sign in to comment.