793cd14b38
This PR improves the message of `unusedVariables` linter, by replacing potentially confusing "unused variable `x`" message with "Variable name `x` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly)." Related issue: https://github.com/leanprover/lean4/issues/13269
154 lines
7.5 KiB
Text
154 lines
7.5 KiB
Text
linterUnusedVariables.lean:18:21-18:22: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:19:6-19:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:24:8-24:9: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:40:5-40:6: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:45:5-45:6: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:48:7-48:8: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:51:8-51:9: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:55:9-55:10: warning: Variable name `z` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:57:11-57:12: warning: Variable name `z` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:62:14-62:15: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:68:20-68:21: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:73:34-73:38: warning: Variable name `inst` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:114:25-114:26: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:115:6-115:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:121:6-121:7: warning: Variable name `a` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:131:26-131:27: warning: Variable name `z` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:140:9-140:10: warning: Variable name `h` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:154:8-154:9: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:157:28-157:29: warning: Variable name `β` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:158:7-158:8: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:168:6-168:7: warning: Variable name `s` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:192:6-192:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:202:19-202:20: warning: Variable name `x` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:206:6-206:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:211:6-211:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:216:6-216:7: warning: Variable name `y` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:227:32-227:33: warning: Variable name `b` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|
|
linterUnusedVariables.lean:245:27-245:28: error: don't know how to synthesize placeholder
|
|
context:
|
|
a : Nat
|
|
⊢ Nat
|
|
linterUnusedVariables.lean:246:0-246:7: warning: declaration uses `sorry`
|
|
linterUnusedVariables.lean:247:0-247:7: warning: declaration uses `sorry`
|
|
linterUnusedVariables.lean:248:27-248:29: error: unsolved goals
|
|
a : Nat
|
|
⊢ Nat
|
|
linterUnusedVariables.lean:249:33-249:40: error: unsolved goals
|
|
a : Nat
|
|
⊢ Nat
|
|
linterUnusedVariables.lean:249:0-249:40: error: type of theorem `async` is not a proposition
|
|
Nat → Nat
|
|
linterUnusedVariables.lean:284:41-284:43: warning: Variable name `ha` is not explicitly referenced.
|
|
|
|
The binding can be removed (if unused) or named `_` (if used implicitly).
|
|
|
|
Note: This linter can be disabled with `set_option linter.unusedVariables false`
|