Def outputMessage

Modification history

2024-08-27 23:34

Mathlib/Tactic/Linter/TextBased.lean

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

Deleted outputMessage 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) …

Modified outputMessage View on Github →

2024-06-21 07:01

Mathlib/Tactic/Linter/TextBased.lean

feat: rewrite file length check in Lean (#13620) …

Added outputMessage View on Github →