spelling

leanprover-community · Oct 9, 2024 · 62cea5c · 62cea5c
1 parent bca3ad6
commit 62cea5c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
@@ -91,7 +91,7 @@ def getNames : Syntax → Array Syntax
     if kind == ``Lean.Parser.Command.declId then rargs.push stx else rargs
   | _ => default
 
-/-- The `checkDeclID` linter: it this linter emits a warning, then a declID is considered
+/-- The `checkDeclID` linter: if this linter emits a warning, then a declID is considered
 non-standard style. Currently we only check if it contains a double underscore ("__") as a
 substring.