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