diff --git a/Mathlib/Tactic/Linter/PPRoundtrip.lean b/Mathlib/Tactic/Linter/PPRoundtrip.lean index dced1f5293546..df238e0927ee3 100644 --- a/Mathlib/Tactic/Linter/PPRoundtrip.lean +++ b/Mathlib/Tactic/Linter/PPRoundtrip.lean @@ -60,7 +60,7 @@ def polishSource (s : String) : String × Array Nat := let preWS := split.foldl (init := #[]) fun p q => let txt := q.trimLeft.length (p.push (q.length - txt)).push txt - let preWS := preWS.eraseIdx! 0 + let preWS := preWS.eraseIdxIfInBounds 0 let s := (split.map .trimLeft).filter (· != "") (" ".intercalate (s.filter (!·.isEmpty)), preWS)