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
3 lines
96 B
Text
3 lines
96 B
Text
Val.bool true : Val
|
|
0 : Val
|
|
constProp.lean:659:0-659:5: warning: using 'exit' to interrupt Lean
|