lean4/tests/elab/3705.lean.out.expected at master - lean4 - Gitea: Git with a cup of tea

sdgoij/lean4

mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

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

5 lines

223 B

Plaintext

Raw Permalink Blame History

 .lean:17:9-17:29: warning: declaration uses `sorry`
 .lean:17:9-17:29: warning: declaration uses `sorry`
 .lean:23:0-23:7: warning: declaration uses `sorry`
 .lean:30:8-30:11: warning: declaration uses `sorry`