Def Mathlib.Linter.OneLineAlignLinter.getLinterOneLineAlign

Modification history

2024-07-19 17:46
Mathlib/Tactic/Linter/Lint.lean
chore: remove `#align`-oriented linters (#14909) …
Deleted Mathlib.Linter.OneLineAlignLinter.getLinterOneLineAlignView on Github →
2024-07-11 18:34
Mathlib/Tactic/Linter/Lint.lean
feat: the one-line-align linter (#14322) …
Added Mathlib.Linter.OneLineAlignLinter.getLinterOneLineAlignView on Github →