feat: Add double empty Lint

HepLean/AnomalyCancellation/Basic.lean

@@ -108,7 +108,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
   add_zero S := by
     apply LinSols.ext
     exact χ.chargesAddCommMonoid.add_zero _
-  nsmul n S := ⟨n  • S.val, by
+  nsmul n S := ⟨n • S.val, by
     intro i
     rw [nsmul_eq_smul_cast ℚ]
     erw [(χ.linearACCs i).map_smul, S.linearSol i]
@@ -122,7 +122,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
 /-- An instance providing the operations and properties for `LinSols` to form an
   module over `ℚ`. -/
 @[simps!]
-instance linSolsModule  (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
+instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
   smul a S := ⟨a • S.val, by
     intro i
     rw [(χ.linearACCs i).map_smul, S.linearSol i]
@@ -177,13 +177,13 @@ structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where
 @[ext]
 lemma QuadSols.ext {χ : ACCSystemQuad} {S T : χ.QuadSols} (h : S.val = T.val) :
     S = T := by
-  have h  := ACCSystemLinear.LinSols.ext h
+  have h := ACCSystemLinear.LinSols.ext h
   cases' S
   simp_all only
 
 /-- An instance giving the properties and structures to define an action of `ℚ` on `QuadSols`. -/
 instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols where
-  smul a S :=  ⟨a • S.toLinSols , by
+  smul a S := ⟨a • S.toLinSols , by
     intro i
     erw [(χ.quadraticACCs i).map_smul]
     rw [S.quadSol i]
@@ -198,7 +198,7 @@ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols wher
 
 /-- The inclusion of quadratic solutions into linear solutions. -/
 def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols  where
-  toFun  := QuadSols.toLinSols
+  toFun := QuadSols.toLinSols
   map_smul' _ _ := rfl
 
 /-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion
@@ -239,7 +239,7 @@ def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
 
 /-- An instance giving the properties and structures to define an action of `ℚ` on `Sols`. -/
 instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where
-  smul a S :=  ⟨a • S.toQuadSols , by
+  smul a S := ⟨a • S.toQuadSols, by
     erw [(χ.cubicACC).map_smul]
     rw [S.cubicSol]
     simp⟩

HepLean/AnomalyCancellation/GroupActions.lean

@@ -100,7 +100,7 @@ instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
     rfl
 
 lemma linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
-    (S : χ.QuadSols) :  χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) =
+    (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) =
     G.linSolRep g (χ.quadSolsInclLinSols S) := rfl
 
 lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)

HepLean/AnomalyCancellation/MSSMNu/B3.lean

@@ -37,7 +37,7 @@ def B₃AsCharge : MSSMACC.Charges := toSpecies.symm
     | 1, 2 =>  1
     | 2, 0 => - 1
     | 2, 1 => - 1
-    | 2, 2 =>  1
+    | 2, 2 => 1
     | 3, 0 => - 3
     | 3, 1 => - 3
     | 3, 2 => 3

HepLean/AnomalyCancellation/MSSMNu/Basic.lean

@@ -50,7 +50,7 @@ def splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 →
 /-- An equivalence between `MSSMCharges.charges` and `(Fin 18 → ℚ) × (Fin 2 → ℚ)`. This
 splits the charges up into the SM and the additional ones for the MSSM. -/
 @[simps!]
-def toSplitSMPlusH  : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) :=
+def toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) :=
   toSMPlusH.trans splitSMPlusH
 
 /-- An equivalence between `(Fin 18 → ℚ)` and `(Fin 6 → Fin 3 → ℚ)`. -/
@@ -74,7 +74,7 @@ def toSMSpecies (i : Fin 6) : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charge
   map_add' _ _ := by rfl
   map_smul' _ _ := by rfl
 
-lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f :  (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
+lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) :
     (toSMSpecies i) (toSpecies.symm f) = f.1 i := by
   change (Prod.fst ∘ toSpecies ∘ toSpecies.symm ) _ i= f.1 i
   simp

scripts/double_line_lint.lean

@@ -31,6 +31,15 @@ def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
     else none)
   errors.toArray
 
+/-- Checks if there is a souble space in the line, which is not at the start. -/
+def doubleSpaceLinter : HepLeanTextLinter := fun lines ↦ Id.run do
+  let enumLines := (lines.toList.enumFrom 1)
+  let errors := enumLines.filterMap (fun (lno, l) ↦
+    if String.containsSubstr l.trimLeft "  " then
+      some (s!" Non-initial double space in line. ", lno)
+    else none)
+  errors.toArray
+
 structure HepLeanErrorContext where
   /-- The underlying `message`. -/
   error : String
@@ -47,7 +56,7 @@ def hepLeanLintFile (path : FilePath) : IO Bool := do
   let lines ← IO.FS.lines path
   let allOutput := (Array.map (fun lint ↦
     (Array.map (fun (e, n) ↦ HepLeanErrorContext.mk e n path)) (lint lines)))
-    #[doubleEmptyLineLinter]
+    #[doubleEmptyLineLinter, doubleSpaceLinter]
   let errors := allOutput.flatten
   printErrors errors
   return errors.size > 0