Commit 2024-08-19 15:57 e9f05995

View on Github →

fix: disable the dollarSyntax linter by default (#15970) And move the linter to the Style namespace.

Estimated changes

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Mathlib.Linter.DollarSyntaxLinter.dollarSyntaxLinter

deleted def Mathlib.Linter.DollarSyntaxLinter.findDollarSyntax

added def Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter

added def Mathlib.Linter.Style.dollarSyntax.findDollarSyntax

Modified lakefile.lean