Commit 2024-06-19 08:39 60fd11f2

View on Github →

feat: rewrite set_option style linter in lean (#12928) Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Linter.lean

Created Mathlib/Tactic/Linter/Style.lean

added def Mathlib.Linter.Style.SetOption.getLinterHash

added def Mathlib.Linter.Style.SetOption.is_set_option

added def Mathlib.Linter.Style.SetOption.parse_set_option

added def Mathlib.Linter.Style.SetOption.setOptionLinter

Modified scripts/lint-style.py

Modified test/Explode.lean

Modified test/LibrarySearch/IsCompact.lean

Modified test/LibrarySearch/basic.lean

Modified test/Recall.lean

Modified test/delabLinearIndependent.lean

Created test/lint_style.lean

added theorem foo'

added theorem tactic2

added theorem tactic3

added theorem tactic4

added theorem tactic

Modified test/vec_notation.lean