Compiles now... to be polished!

Mathlib/Tactic/Linter/TextBased.lean

@@ -323,28 +323,31 @@ 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
-  for i in [0::lines.size - 1] do
-    let line := lines[i]
+  let mut i := 0
+  for line in lines do
     if line.back == ' ' then
       errors := errors.push (StyleError.trailingWhitespace, i + 1)
-      fixedLines := fixedLines.set! 0 (line.dropRightWhile (· == ' '))
+      fixedLines := fixedLines.set! i (line.dropRightWhile (· == ' '))
+    i := i + 1
   return (errors, fixedLines)
 -- xxx: can I avoid set!, as I know the index is inbounds? is there a better way?
 -- ask on zulip for the most idiomatic construct
 
 -- TODO: apply the same change to all other linters, once this has been tested...
 
-def semicolonLinter : TextbaseLinter := fun lines ↦ Id.run do
+def semicolonLinter : TextbasedLinter := fun lines ↦ Id.run do
   let mut errors := Array.mkEmpty 0
   let mut fixedLines := lines
-  for i in [0::lines.size - 1] do
-    let line := lines[i]
+  let mut idx := 0
+  for line in lines do--for i in [0::lines.size - 1] do
+    --let line := lines[i]
     if line.contains ';' then
       let replaced := (line.replace " ;" "; ").replace "  " " "
       if replaced != line then
-        errors := errors.push (StyleError.semicolon, i + 1) -- TODO: add error variant etc!
+        -- errors := errors.push (StyleError.semicolon, idx + 1) -- TODO: add error variant etc!
         -- "Line contains a space before a semicolon"
-        fixedLines := fixedLines.set! 0 replaced
+        fixedLines := fixedLines.set! idx replaced
+    idx := idx+ 1
   return (errors, fixedLines)
 
 /-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.