Skip to content

chore: change UnusedSimpArgs hint #14313

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wkrozowski merged 1 commit into from
Jul 8, 2026
+20 −20
Merged

chore: change UnusedSimpArgs hint #14313

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Lean/Linter/UnusedSimpArgs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ private def warnUnused (stx : Syntax) (i : Nat) : CoreM Unit := do
otherArgs := otherArgs.push simpArgs[j]
let stx' := Tactic.setSimpParams stx otherArgs
let suggestion : Meta.Hint.Suggestion := stx'
let suggestion := { suggestion with span? := stx }
let suggestion := { suggestion with span? := stx, diffGranularity := .none }
let mut hint ← MessageData.hint "Omit it from the simp argument list." #[ suggestion ]
-- Add hint about `←`
let isInv := argStx.getKind == ``Lean.Parser.Tactic.simpLemma && !argStx[1].isNone
Expand Down
4 changes: 2 additions & 2 deletions tests/elab/12559.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ warning: This simp argument is unused:
False

Hint: Omit it from the simp argument list.
simp ̵[̵F̵a̵l̵s̵e̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -30,7 +30,7 @@ warning: This simp argument is unused:
False

Hint: Omit it from the simp argument list.
simp ̵[̵F̵a̵l̵s̵e̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand Down
34 changes: 17 additions & 17 deletions tests/elab/simpUnusedArgs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ warning: This simp argument is unused:
id_eq

Hint: Omit it from the simp argument list.
simp ̵[̵i̵d̵_̵e̵q̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -24,7 +24,7 @@ warning: This simp argument is unused:
id_eq

Hint: Omit it from the simp argument list.
simp [i̵d̵_̵e̵q̵,̵ ̵and_self]
[apply] simp [and_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -39,7 +39,7 @@ warning: This simp argument is unused:
some_def

Hint: Omit it from the simp argument list.
simp ̵[̵s̵o̵m̵e̵_̵d̵e̵f̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -58,15 +58,15 @@ warning: This simp argument is unused:
some_def.eq_def

Hint: Omit it from the simp argument list.
simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
[apply] simp [some_def, some_def.eq_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
---
warning: This simp argument is unused:
some_def.eq_def

Hint: Omit it from the simp argument list.
simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
[apply] simp [some_def, some_def.eq_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -77,15 +77,15 @@ warning: This simp argument is unused:
(some_def.eq_def)

Hint: Omit it from the simp argument list.
simp [some_def, (̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵)̵,̵ ̵some_def.eq_def]
[apply] simp [some_def, some_def.eq_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
---
warning: This simp argument is unused:
some_def.eq_def

Hint: Omit it from the simp argument list.
simp [some_def, (some_def.eq_def),̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
[apply] simp [some_def, (some_def.eq_def)]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -106,7 +106,7 @@ warning: This simp argument is unused:
some_rdef

Hint: Omit it from the simp argument list.
simp -failIfUnchanged ̵[̵s̵o̵m̵e̵_̵r̵d̵e̵f̵]̵
[apply] simp -failIfUnchanged

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -121,7 +121,7 @@ warning: This simp argument is unused:
some_rdef.eq_def

Hint: Omit it from the simp argument list.
simp -failIfUnchanged [some_rdef,̵ ̵s̵o̵m̵e̵_̵r̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
[apply] simp -failIfUnchanged [some_rdef]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand Down Expand Up @@ -160,7 +160,7 @@ warning: This simp argument is unused:
_h

Hint: Omit it from the simp argument list.
simp -failIfUnchanged ̵[̵_̵h̵]̵
[apply] simp -failIfUnchanged

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -178,7 +178,7 @@ warning: This simp argument is unused:
↓reduceIte

Hint: Omit it from the simp argument list.
simp only [↓reduceI̵t̵e̵,̵ ̵↓̵r̵e̵d̵u̵c̵e̵DIte]
[apply] simp only [↓reduceDIte]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -202,7 +202,7 @@ warning: This simp argument is unused:
x

Hint: Omit it from the simp argument list.
simp ̵[̵x̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -216,7 +216,7 @@ warning: This simp argument is unused:
h3

Hint: Omit it from the simp argument list.
simp [h1, h2,̵ ̵h̵3̵]
[apply] simp [h1, h2]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -229,15 +229,15 @@ warning: This simp argument is unused:
h2

Hint: Omit it from the simp argument list.
simp [h1,̵ ̵h̵2̵]
[apply] simp [h1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
---
warning: This simp argument is unused:
h1

Hint: Omit it from the simp argument list.
simp [h1̵,̵ ̵h̵2]
[apply] simp [h2]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand All @@ -257,7 +257,7 @@ warning: This simp argument is unused:
h

Hint: Omit it from the simp argument list.
simp ̵[̵h̵]̵
[apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
Expand Down Expand Up @@ -304,7 +304,7 @@ warning: This simp argument is unused:
← ab

Hint: Omit it from the simp argument list.
simp ̵[̵←̵ ̵a̵b̵]̵
[apply] simp

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Expand Down
Loading