Commit 2025-05-19 10:23 e262afd1

View on Github →

fix(docstring linter): inspect also internal docstrings (#24673) This omission was pointed out in #24532.

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Homology.lean

Modified Mathlib/CategoryTheory/EpiMono.lean

Modified Mathlib/Tactic/FunProp/Types.lean

Modified Mathlib/Tactic/Linter/DocString.lean

added def Mathlib.Linter.deindentString

added def Mathlib.Linter.getDeclModifiers

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

Modified Mathlib/Topology/CWComplex/Classical/Finite.lean

Modified MathlibTest/DocString.lean

added structure X