37f10435a9
This PR changes the way the linting for `linter.unusedSimpArgs` gets the value from the environment. This is achieved by using the appropriate helper functions defined in `Lean.Linter.Basic`. The following now compiles without warning ```lean4 set_option linter.all false in example : True := by simp [False] ``` Fixes #12559
43 lines
817 B
Text
43 lines
817 B
Text
/-!
|
|
# Make `linter.all` option also control the `linter.unusedSimpArgs` linter
|
|
|
|
https://github.com/leanprover/lean4/issues/12559 -/
|
|
|
|
section
|
|
|
|
set_option linter.unusedSimpArgs true
|
|
|
|
/--
|
|
warning: This simp argument is unused:
|
|
False
|
|
|
|
Hint: Omit it from the simp argument list.
|
|
simp ̵[̵F̵a̵l̵s̵e̵]̵
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by simp [False]
|
|
|
|
end
|
|
|
|
section
|
|
|
|
set_option linter.all true
|
|
|
|
/--
|
|
warning: This simp argument is unused:
|
|
False
|
|
|
|
Hint: Omit it from the simp argument list.
|
|
simp ̵[̵F̵a̵l̵s̵e̵]̵
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by simp [False]
|
|
|
|
set_option linter.all false in
|
|
example : True := by simp [False]
|
|
|
|
end
|