We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b9e3582 commit 930f60fCopy full SHA for 930f60f
Mathlib/Tactic/Linter/TextBased.lean
@@ -337,8 +337,7 @@ def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
337
def semicolonLinter : TextbasedLinter := fun lines ↦ Id.run do
338
let mut errors := Array.mkEmpty 0
339
let mut fixedLines := lines
340
- for h : idx in [:lines.size] do
341
- let line := lines[idx]
+ for (line, idx) in lines.zipWithIndex do
342
let pos := line.find (· == ';')
343
if pos != line.endPos then
344
if line.get (line.prev pos) == ' ' then
0 commit comments