Def lint_style

Modification history

2024-08-09 00:58

scripts/lint-style.lean

refactor: polish `lint_style` and rename to lint-style (#14757) …

Deleted lint_style View on Github →

2024-06-24 11:40

Mathlib/Tactic/Linter/TextBased.lean

chore: move `lint_style` executable to the `scripts` directory (#14057) …

Modified lint_style View on Github →

2024-06-23 07:52

Mathlib/Tactic/Linter/TextBased.lean

feat(lint-style): fix `update-style-exceptions.py`; produce human-readable output by default (#14012) …

Added lint_style View on Github →