use eraseIdxIfInBounds

leanprover-community · Nov 21, 2024 · 5797528 · 5797528
1 parent 13b4529
commit 5797528
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)