Def parse?_errorContext

Modification history

2024-08-27 23:34

Mathlib/Tactic/Linter/TextBased.lean

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

Deleted parse?_errorContext View on Github →

2024-06-21 07:01

Mathlib/Tactic/Linter/TextBased.lean

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

Added parse?_errorContext View on Github →