Def Mathlib.Linter.deindentString

Modification history

2025-05-19 10:23
Mathlib/Tactic/Linter/DocString.lean
fix(docstring linter): inspect also internal docstrings (#24673) …
Added Mathlib.Linter.deindentStringView on Github →