Commit 2024-09-04 22:48 622c6624

View on Github →

chore: move style linters to the style namespace (#16265) Redone version of #15971.

Estimated changes

Modified Mathlib/Data/QPF/Multivariate/Basic.lean

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Mathlib.Linter.CDotLinter.cdotLinter

deleted def Mathlib.Linter.LongLine.longLineLinter

deleted def Mathlib.Linter.MissingEnd.missingEndLinter

added def Mathlib.Linter.Style.cdotLinter

added def Mathlib.Linter.Style.longLine.longLineLinter

added def Mathlib.Linter.Style.missingEnd.missingEndLinter

Modified lakefile.lean

Modified test/Lint.lean

Modified test/RewriteSearch/Basic.lean

Modified test/Use.lean

Modified test/fun_prop.lean

Modified test/fun_prop_dev.lean

Modified test/polyrith.lean