Def Mathlib.Linter.DollarSyntaxLinter.dollarSyntaxLinter

Modification history

2024-08-19 15:57
Mathlib/Tactic/Linter/Lint.lean
fix: disable the dollarSyntax linter by default (#15970) …
Deleted Mathlib.Linter.DollarSyntaxLinter.dollarSyntaxLinterView on Github →
2024-08-19 07:41
Mathlib/Tactic/Linter/Lint.lean
feat: the dollarSyntax linter (#15909) …
Added Mathlib.Linter.DollarSyntaxLinter.dollarSyntaxLinterView on Github →