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
9 lines
411 B
Text
9 lines
411 B
Text
warningAsError.lean:8:6-8:7: warning: `g` has been deprecated: Use `f` instead
|
|
1
|
|
warningAsError.lean:12:6-12:7: error: `g` has been deprecated: Use `f` instead
|
|
1
|
|
warningAsError.lean:15:7-15:13: error: Variable name `unused` 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`
|