Commit 2024-07-19 17:46 5473f375

View on Github →

chore: remove #align-oriented linters (#14909) Now that #aligns have been removed, these linters and exceptions are obsolete.

Estimated changes

Modified Mathlib/Tactic/Linter/HashCommandLinter.lean

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Mathlib.Linter.OneLineAlignLinter.getLinterOneLineAlign

deleted def Mathlib.Linter.OneLineAlignLinter.oneLineAlign

Modified test/HashCommandLinter.lean

deleted theorem fo₁