Def Mathlib.Linter.whitespaceLinter

Modification history

2026-01-07 21:30

Mathlib/Tactic/Linter/Whitespace.lean

chore: rename the `commandStart` linter to `whitespace` (#33708) …

Added Mathlib.Linter.whitespaceLinter View on Github →