lean4-htt/tests/elab/5755.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

3 lines

166 B

Text

Raw Permalink Blame History

	5755.lean:15:8-15:25: warning: declaration uses `sorry`
	5755.lean:25:0-25:7: warning: declaration uses `sorry`
	5755.lean:46:0-46:7: warning: declaration uses `sorry`