Commit 2024-11-22 01:48 1f86e43e

View on Github →

feat: rewrite the trailing whitespace linter in Lean (#16334)

Estimated changes

Modified Mathlib/Tactic/Linter/TextBased.lean

added def Mathlib.Linter.TextBased.trailingWhitespaceLinter

Modified scripts/lint-style.py