Def Lean.Syntax.Mathlib.Linter.EmptyLine.emptyLineLinter

Modification history

2025-11-26 08:45
Mathlib/Tactic/Linter/EmptyLine.lean
feat: the empty line in commands linter (#25945) …
Added Lean.Syntax.Mathlib.Linter.EmptyLine.emptyLineLinterView on Github →