lean4-htt/tests/elab/simpDischargeLoop.lean.out.expected at master - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

fiforeach 37f10435a9

fix: make option linter.unusedSimpArgs respect linter.all (#12560 )

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

2026-03-09 15:12:02 +00:00

1 line

69 B

Text

Raw Permalink Blame History

simpDischargeLoop.lean:42:8-42:21: warning: declaration uses `sorry`