Commit 2024-08-29 00:16 172492c1

View on Github →

chore: move linter.setOption to the style namespace (#16212) Extracted from #15971.

Estimated changes

Modified Mathlib/Tactic/Linter/Style.lean

deleted def Mathlib.Linter.Style.SetOption.is_set_option

deleted def Mathlib.Linter.Style.SetOption.parse_set_option

deleted def Mathlib.Linter.Style.SetOption.setOptionLinter

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 lakefile.lean

Modified test/Explode.lean

Modified test/LibrarySearch/basic.lean

Modified test/LintStyle.lean

Modified test/Recall.lean

Modified test/delabLinearIndependent.lean

Modified test/vec_notation.lean