Def Mathlib.Linter.commandStartLinter

Modification history

2026-01-07 21:30
Mathlib/Tactic/Linter/Whitespace.lean
chore: rename the `commandStart` linter to `whitespace` (#33708) …
Deleted Mathlib.Linter.commandStartLinterView on Github →
2025-06-17 18:33
Mathlib/Tactic/Linter/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Mathlib.Linter.commandStartLinterView on Github →