Def Mathlib.Linter.CommandStart.endPos

Modification history

2025-06-17 18:33
Mathlib/Tactic/Linter/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Mathlib.Linter.CommandStart.endPosView on Github →