Commit 2024-11-27 12:13 671c0905

View on Github →

chore: move style linters to Style (#19529) This makes for a more coherent split of the linter files. Third attempt after #15942 and #16510.

Estimated changes

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Mathlib.Linter.Style.cdotLinter

deleted def Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter

deleted def Mathlib.Linter.Style.dollarSyntax.findDollarSyntax

deleted def Mathlib.Linter.Style.lambdaSyntax.findLambdaSyntax

deleted def Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter

deleted def Mathlib.Linter.Style.longFile.longFileLinter

deleted def Mathlib.Linter.Style.longLine.longLineLinter

deleted def Mathlib.Linter.Style.missingEnd.missingEndLinter

deleted def Mathlib.Linter.findCDot

deleted def Mathlib.Linter.isCDot?

deleted def Mathlib.Linter.unwanted_cdot

Modified Mathlib/Tactic/Linter/Style.lean

added def Mathlib.Linter.Style.cdotLinter

added def Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter

added def Mathlib.Linter.Style.dollarSyntax.findDollarSyntax

added def Mathlib.Linter.Style.lambdaSyntax.findLambdaSyntax

added def Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter

added def Mathlib.Linter.Style.longFile.longFileLinter

added def Mathlib.Linter.Style.longLine.longLineLinter

added def Mathlib.Linter.Style.missingEnd.missingEndLinter

added def Mathlib.Linter.findCDot

added def Mathlib.Linter.isCDot?

added def Mathlib.Linter.unwanted_cdot

Modified MathlibTest/Lint.lean

deleted def foo

Modified MathlibTest/LintStyle.lean

added def foo

Modified MathlibTest/LongFile.lean