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
24 lines
650 B
Text
24 lines
650 B
Text
set_option linter.unusedVariables true
|
|
|
|
class Foo
|
|
|
|
def bar [Foo] := 0
|
|
|
|
/--
|
|
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`
|
|
-/
|
|
#guard_msgs in
|
|
def baz := let x := Foo.mk; bar -- unused variable `x`
|
|
|
|
/--
|
|
error: failed to synthesize instance of type class
|
|
Foo
|
|
|
|
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
|
|
-/
|
|
#guard_msgs in
|
|
def baz':= bar -- failed to synthesize instance of type class Foo
|