Def Mathlib.Linter.TextBased.checkFileLength

Modification history

2024-08-29 18:57

Mathlib/Tactic/Linter/TextBased.lean

chore: remove the text-based line length linter (#16269) …

Deleted Mathlib.Linter.TextBased.checkFileLength View on Github →

2024-08-27 23:34

Mathlib/Tactic/Linter/TextBased.lean

chore(Linter/TextBased): namespace declarations (#16203) …

Added Mathlib.Linter.TextBased.checkFileLength View on Github →