wip: fix line numbers; untested

leanprover-community · Sep 5, 2024 · fa9b485 · fa9b485
1 parent 4524784
commit fa9b485
Showing 1 changed file with 3 additions and 6 deletions.
diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
@@ -323,14 +323,11 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
 def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
   let mut errors := Array.mkEmpty 0
   let mut fixedLines := lines
-  -- invariant: this equals the current index of 'line' in 'lines',
-  -- hence starts at 0 and is incremented *at the end* of the loop
-  let mut lineNumber := 0
-  for line in lines do
+  for i in [0::lines.size -1] do
+    let line := lines[i]
     if line.back == ' ' then
-      errors := errors.push (StyleError.trailingWhitespace, lineNumber)
+      errors := errors.push (StyleError.trailingWhitespace, i + 1)
       fixedLines := fixedLines.set! 0 (line.dropRightWhile (· == ' '))
-    lineNumber := lineNumber + 1
   return (errors, fixedLines)