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
This commit is contained in:
fiforeach
GitHub
parent
a4dd66df62
commit
37f10435a9
32 changed files with 46 additions and 432 deletions
|
|
@ -690,7 +690,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
|
|||
simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
traceSimpCall stx stats.usedTheorems
|
||||
else if linter.unusedSimpArgs.get (← getOptions) then
|
||||
else if Linter.getLinterValue linter.unusedSimpArgs (← Linter.getLinterOptions) then
|
||||
withRef stx do
|
||||
warnUnusedSimpArgs simpArgs stats.usedTheorems
|
||||
return stats.diag
|
||||
|
|
@ -707,7 +707,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
|
|||
| some mvarId => replaceMainGoal [mvarId]
|
||||
if tactic.simp.trace.get (← getOptions) then
|
||||
traceSimpCall stx stats.usedTheorems
|
||||
else if linter.unusedSimpArgs.get (← getOptions) then
|
||||
else if Linter.getLinterValue linter.unusedSimpArgs (← Linter.getLinterOptions) then
|
||||
withRef stx do
|
||||
warnUnusedSimpArgs simpArgs stats.usedTheorems
|
||||
return stats.diag
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ private def warnUnused (stx : Syntax) (i : Nat) : CoreM Unit := do
|
|||
|
||||
def unusedSimpArgs : Linter where
|
||||
run cmdStx := do
|
||||
if !Tactic.linter.unusedSimpArgs.get (← getOptions) then return
|
||||
if !getLinterValue Tactic.linter.unusedSimpArgs (← getLinterOptions) then return
|
||||
let some cmdStxRange := cmdStx.getRange? | return
|
||||
|
||||
let infoTrees := (← get).infoState.trees.toArray
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
1184.lean:4:30-4:31: warning: This simp argument is unused:
|
||||
h
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp (disch := assumption) ̵[̵h̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
43
tests/elab/12559.lean
Normal file
43
tests/elab/12559.lean
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
/-!
|
||||
# Make `linter.all` option also control the `linter.unusedSimpArgs` linter
|
||||
|
||||
https://github.com/leanprover/lean4/issues/12559 -/
|
||||
|
||||
section
|
||||
|
||||
set_option linter.unusedSimpArgs true
|
||||
|
||||
/--
|
||||
warning: This simp argument is unused:
|
||||
False
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵F̵a̵l̵s̵e̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : True := by simp [False]
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
|
||||
set_option linter.all true
|
||||
|
||||
/--
|
||||
warning: This simp argument is unused:
|
||||
False
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵F̵a̵l̵s̵e̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : True := by simp [False]
|
||||
|
||||
set_option linter.all false in
|
||||
example : True := by simp [False]
|
||||
|
||||
end
|
||||
|
|
@ -1,18 +1,4 @@
|
|||
3705.lean:17:9-17:29: warning: declaration uses `sorry`
|
||||
3705.lean:17:9-17:29: warning: declaration uses `sorry`
|
||||
3705.lean:23:0-23:7: warning: declaration uses `sorry`
|
||||
3705.lean:27:54-27:62: warning: This simp argument is unused:
|
||||
mul_comm
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp (config := { failIfUnchanged := false }) only ̵[̵m̵u̵l̵_̵c̵o̵m̵m̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
3705.lean:30:8-30:11: warning: declaration uses `sorry`
|
||||
3705.lean:33:13-33:21: warning: This simp argument is unused:
|
||||
mul_comm
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only ̵[̵m̵u̵l̵_̵c̵o̵m̵m̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
4947.lean:6:41-6:54: warning: This simp argument is unused:
|
||||
Nat.reducePow
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only ̵[̵N̵a̵t̵.̵r̵e̵d̵u̵c̵e̵P̵o̵w̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,10 +1,3 @@
|
|||
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`
|
||||
5755.lean:47:8-47:9: warning: This simp argument is unused:
|
||||
f
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵f̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
|
|||
|
|
@ -11,35 +11,5 @@
|
|||
6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
|
||||
6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
|
||||
6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry`
|
||||
6123_cat_adjunction.lean:481:67-481:71: warning: This simp argument is unused:
|
||||
of_α
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
6123_cat_adjunction.lean:481:73-481:78: warning: This simp argument is unused:
|
||||
id_eq
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α,̵ ̵i̵d̵_̵e̵q̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
|
||||
6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry`
|
||||
6123_cat_adjunction.lean:496:45-496:49: warning: This simp argument is unused:
|
||||
of_α
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
|
||||
Functor.comp_map, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
6123_cat_adjunction.lean:496:51-496:56: warning: This simp argument is unused:
|
||||
id_eq
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
|
||||
Functor.comp_map, typeToCat_map, of_α,̵ ̵i̵d̵_̵e̵q̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
|
|||
|
|
@ -1,42 +0,0 @@
|
|||
860.lean:26:12-26:20: warning: This simp argument is unused:
|
||||
invImage
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [i̵n̵v̵Im̵a̵g̵e̵,̵ ̵I̵nvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
860.lean:26:22-26:30: warning: This simp argument is unused:
|
||||
InvImage
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [invImage, I̵n̵v̵I̵m̵a̵g̵e̵,̵ ̵Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
860.lean:26:32-26:40: warning: This simp argument is unused:
|
||||
Prod.lex
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [invImage, InvImage, P̵r̵o̵d̵.̵l̵e̵x̵,̵ ̵sizeOfWFRel, measure, Nat.lt_wfRel]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
860.lean:26:42-26:53: warning: This simp argument is unused:
|
||||
sizeOfWFRel
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [invImage, InvImage, Prod.lex, s̵i̵z̵e̵O̵f̵W̵F̵R̵e̵l̵,̵ ̵measure, Nat.lt_wfRel]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
860.lean:26:55-26:62: warning: This simp argument is unused:
|
||||
measure
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [invImage, InvImage, Prod.lex, sizeOfWFRel, m̵e̵a̵s̵u̵r̵e̵,̵ ̵Nat.lt_wfRel]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
860.lean:26:64-26:76: warning: This simp argument is unused:
|
||||
Nat.lt_wfRel
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure,̵ ̵N̵a̵t̵.̵l̵t̵_̵w̵f̵R̵e̵l̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
968.lean:3:39-3:48: warning: This simp argument is unused:
|
||||
and_assoc
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
968.lean:7:39-7:48: warning: This simp argument is unused:
|
||||
and_assoc
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
972.lean:19:38-19:47: warning: This simp argument is unused:
|
||||
mul_assoc
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [mul_left_comm, mul_comm,̵ ̵m̵u̵l̵_̵a̵s̵s̵o̵c̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
972.lean:22:28-22:36: warning: This simp argument is unused:
|
||||
mul_comm
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [mul_left_comm, mul_c̵o̵m̵m̵,̵ ̵m̵u̵l̵_̵assoc]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
972.lean:22:38-22:47: warning: This simp argument is unused:
|
||||
mul_assoc
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [mul_left_comm, mul_comm,̵ ̵m̵u̵l̵_̵a̵s̵s̵o̵c̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,10 +1,3 @@
|
|||
ac_expr.lean:95:16-95:22: warning: This simp argument is unused:
|
||||
denote
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [d̵e̵n̵o̵t̵e̵,̵ ̵ih]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
theorem ex₂ : ∀ (x₁ x₂ x₃ x₄ : Nat), x₁ + x₂ + (x₃ + x₄) = x₃ + x₁ + x₂ + x₄ :=
|
||||
fun x₁ x₂ x₃ x₄ =>
|
||||
Expr.eq_of_sort_flat
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
bv_uninterpreted.lean:9:8-9:9: warning: This simp argument is unused:
|
||||
h
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵h̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,24 +1,3 @@
|
|||
Val.bool true : Val
|
||||
0 : Val
|
||||
constProp.lean:389:22-389:25: warning: This simp argument is unused:
|
||||
hnp
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [̵h̵n̵p̵]̵ ̵at ih₂
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
constProp.lean:542:8-542:11: warning: This simp argument is unused:
|
||||
hxy
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [h̵x̵y̵,̵ ̵Ne.symm hxy] at hf
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
constProp.lean:595:10-595:13: warning: This simp argument is unused:
|
||||
heq
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [̵h̵e̵q̵]̵ ̵at ih₄
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
constProp.lean:659:0-659:5: warning: using 'exit' to interrupt Lean
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
eq_some_iff_get_eq_issue.lean:6:8-6:19: warning: This simp argument is unused:
|
||||
exists_prop
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵e̵x̵i̵s̵t̵s̵_̵p̵r̵o̵p̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
funInduction.lean:378:47-378:55: warning: This simp argument is unused:
|
||||
Finn.min
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
funInduction.lean:381:48-381:57: warning: This simp argument is unused:
|
||||
Finn.min'
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
funInduction.lean:384:49-384:59: warning: This simp argument is unused:
|
||||
Finn.min''
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵'̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
funinduction_ident.lean:312:39-312:47: warning: This simp argument is unused:
|
||||
Finn.min
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
funinduction_ident.lean:315:40-315:49: warning: This simp argument is unused:
|
||||
Finn.min'
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
funinduction_ident.lean:318:41-318:51: warning: This simp argument is unused:
|
||||
Finn.min''
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all [Finn.m̵i̵n̵'̵'̵,̵ ̵F̵i̵n̵n̵.̵le]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -18,13 +18,6 @@ Try this:
|
|||
grind_qsort.lean:55:8-55:40: warning: declaration uses `sorry`
|
||||
grind_qsort.lean:62:8-62:40: warning: declaration uses `sorry`
|
||||
grind_qsort.lean:68:8-68:34: warning: declaration uses `sorry`
|
||||
grind_qsort.lean:74:39-74:60: warning: This simp argument is unused:
|
||||
List.getElem?_toArray
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp_all only [perm_iff_toList_perm, L̵i̵s̵t̵.̵g̵e̵t̵E̵l̵e̵m̵?̵_̵t̵o̵A̵r̵r̵a̵y̵,̵ ̵List.extract_toArray, List.extract_eq_take_drop]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
Try these:
|
||||
[apply] [grind .] for pattern: [@Perm #7 (@extract _ #6 #3 #2) (@extract _ #5 #3 #2)]
|
||||
[apply] [grind =>] for pattern: [@Perm #7 #6 #5, @Perm _ (@extract _ #6 #3 #2) (@extract _ #5 #3 #2)]
|
||||
|
|
|
|||
|
|
@ -7,10 +7,3 @@ gring_11543.lean:65:9-65:30: warning: declaration uses `sorry`
|
|||
gring_11543.lean:74:8-74:20: warning: declaration uses `sorry`
|
||||
gring_11543.lean:91:8-91:22: warning: declaration uses `sorry`
|
||||
gring_11543.lean:123:8-123:28: warning: declaration uses `sorry`
|
||||
gring_11543.lean:173:52-173:66: warning: This simp argument is unused:
|
||||
add_sub_cancel
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [mul_sub_left_distrib, ← add_sub_assoc, a̵d̵d̵_̵s̵u̵b̵_̵c̵a̵n̵c̵e̵l̵,̵ ̵tsub_le_iff_right] at this
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
|
|||
|
|
@ -1,84 +0,0 @@
|
|||
issue11181.lean:6:26-6:35: warning: This simp argument is unused:
|
||||
instXorOp
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, i̵n̵s̵t̵X̵o̵r̵O̵p̵,̵ ̵xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:6:37-6:40: warning: This simp argument is unused:
|
||||
xor
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, x̵o̵r̵,̵ ̵bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:6:42-6:49: warning: This simp argument is unused:
|
||||
bitwise
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, b̵i̵t̵w̵i̵s̵e̵,̵ ̵Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:6:51-6:64: warning: This simp argument is unused:
|
||||
Bool.bne_true
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, B̵o̵o̵l̵.̵b̵n̵e̵_̵t̵r̵u̵e̵,̵ ̵Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:6:66-6:80: warning: This simp argument is unused:
|
||||
Bool.not_false
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, B̵o̵o̵l̵.̵n̵o̵t̵_̵f̵a̵l̵s̵e̵,̵ ̵↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:6:82-6:92: warning: This simp argument is unused:
|
||||
↓reduceIte
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false,̵ ̵↓̵r̵e̵d̵u̵c̵e̵I̵t̵e̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:24-10:33: warning: This simp argument is unused:
|
||||
instXorOp
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, i̵n̵s̵t̵X̵o̵r̵O̵p̵,̵ ̵xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:35-10:38: warning: This simp argument is unused:
|
||||
xor
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, x̵o̵r̵,̵ ̵bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:40-10:47: warning: This simp argument is unused:
|
||||
bitwise
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, b̵i̵t̵w̵i̵s̵e̵,̵ ̵Bool.bne_true, Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:49-10:62: warning: This simp argument is unused:
|
||||
Bool.bne_true
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, B̵o̵o̵l̵.̵b̵n̵e̵_̵t̵r̵u̵e̵,̵ ̵Bool.not_false, ↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:64-10:78: warning: This simp argument is unused:
|
||||
Bool.not_false
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, B̵o̵o̵l̵.̵n̵o̵t̵_̵f̵a̵l̵s̵e̵,̵ ̵↓reduceIte]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
issue11181.lean:10:80-10:90: warning: This simp argument is unused:
|
||||
↓reduceIte
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false,̵ ̵↓̵r̵e̵d̵u̵c̵e̵I̵t̵e̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
issue7318.lean:27:38-27:50: warning: This simp argument is unused:
|
||||
Q_of_decide'
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp (discharger := native_decide) [Q_of_decide'̵,̵ ̵Q̵_̵o̵f̵_̵d̵e̵c̵i̵d̵e̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,11 +1,4 @@
|
|||
lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
|
||||
lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
|
||||
lazyListRotateUnfoldProof.lean:18:4-18:10: warning: declaration uses `sorry`
|
||||
lazyListRotateUnfoldProof.lean:21:44-21:59: warning: This simp argument is unused:
|
||||
LazyList.length
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp +arith [̵L̵a̵z̵y̵L̵i̵s̵t̵.̵l̵e̵n̵g̵t̵h̵]̵ ̵at h
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
lazyListRotateUnfoldProof.lean:27:8-27:18: warning: declaration uses `sorry`
|
||||
|
|
|
|||
|
|
@ -1,14 +0,0 @@
|
|||
lazylistThunk.lean:28:17-28:30: warning: This simp argument is unused:
|
||||
length_toList
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp ̵[̵l̵e̵n̵g̵t̵h̵_̵t̵o̵L̵i̵s̵t̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
lazylistThunk.lean:41:30-41:50: warning: This simp argument is unused:
|
||||
toList_force_none as
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [force,̵ ̵t̵o̵L̵i̵s̵t̵_̵f̵o̵r̵c̵e̵_̵n̵o̵n̵e̵ ̵a̵s̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
mutualDefThms.lean:47:74-47:76: warning: This simp argument is unused:
|
||||
ih
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp +arith [foldl_init x.length, foldl_init (_ + _),̵ ̵i̵h̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
simpDecide.lean:16:44-16:51: warning: This simp argument is unused:
|
||||
fib_two
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp (config := { decide := true }) only ̵[̵f̵i̵b̵_̵t̵w̵o̵]̵
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,15 +1 @@
|
|||
simpDischargeLoop.lean:38:12-38:14: warning: This simp argument is unused:
|
||||
ih
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [i̵h̵,̵ ̵double]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
simpDischargeLoop.lean:38:16-38:22: warning: This simp argument is unused:
|
||||
double
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [ih,̵ ̵d̵o̵u̵b̵l̵e̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
simpDischargeLoop.lean:42:8-42:21: warning: declaration uses `sorry`
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
simpMatch.lean:10:26-10:29: warning: This simp argument is unused:
|
||||
hnp
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [̵h̵n̵p̵]̵ ̵at h
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
simpRwBug.lean:4:100-4:102: warning: This simp argument is unused:
|
||||
ih
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [Nat.add_assoc,̵ ̵i̵h̵]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
simpStarHyp.lean:2:12-2:14: warning: This simp argument is unused:
|
||||
h₂
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [h₁,̵ ̵h̵₂̵] at h₁ h₂
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -11,10 +11,3 @@ splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
|
|||
splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
|
||||
splitIssue2.lean:49:4-49:8: warning: declaration uses `sorry`
|
||||
splitIssue2.lean:48:0-57:41: warning: declaration uses `sorry`
|
||||
splitIssue2.lean:64:20-64:39: warning: This simp argument is unused:
|
||||
Array.length_toList
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp only [rootD, A̵r̵r̵a̵y̵.̵l̵e̵n̵g̵t̵h̵_̵t̵o̵L̵i̵s̵t̵,̵ ̵parent_lt]
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
|
|||
|
|
@ -1,14 +0,0 @@
|
|||
treeNode.lean:35:18-35:30: warning: This simp argument is unused:
|
||||
List.flatten
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [̵L̵i̵s̵t̵.̵f̵l̵a̵t̵t̵e̵n̵,̵ ̵n̵u̵m̵N̵a̵m̵e̵s̵L̵s̵t̵]̵[̲n̲u̲m̲N̲a̲m̲e̲s̲L̲s̲t̲]̲
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
treeNode.lean:36:22-36:34: warning: This simp argument is unused:
|
||||
List.flatten
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [List.f̵l̵a̵t̵t̵e̵n̵,̵ ̵L̵i̵s̵t̵.̵map, numNamesLst, length_treeToList_eq_numNames c, helper cs']
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
wfOverapplicationIssue.lean:2:8-2:22: warning: This simp argument is unused:
|
||||
Membership.mem
|
||||
|
||||
Hint: Omit it from the simp argument list.
|
||||
simp [M̵e̵m̵b̵e̵r̵s̵h̵i̵p̵.̵m̵e̵m̵,̵ ̵contains, any, Id.run, BEq.beq, anyM] at h
|
||||
|
||||
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
|
||||
Loading…
Add table
Reference in a new issue