Commit 2024-07-11 18:34 1da7f698

View on Github →

feat: the one-line-align linter (#14322) This linter makes sure that #align statements span a single line.

Estimated changes

Modified Mathlib/CategoryTheory/Closed/Functor.lean

Modified Mathlib/Tactic/Linter/Lint.lean

added def Mathlib.Linter.OneLineAlignLinter.getLinterOneLineAlign

added def Mathlib.Linter.OneLineAlignLinter.oneLineAlign

Modified test/Lint.lean

added theorem toAlign