Unused variables and proof_wanted

Stream: general

[Yaël Dillies]

proof_wanted statements get linted for unused variables. Doesn't seem very fair to me :grinning:

[Mario Carneiro]

It's possible to add ignore fns for unused variables (although IIRC there is some issue with the environment extension which makes this not actually work, cc: @Sebastian Ullrich )

[Andrew Yang]

Bump. proof_wanted isn't really usable in mathlib because of this.

[Yaël Dillies]

For now, you can set_option linter.unusedVariables false in at least

[Martin Dvořák]

Bump (same complaint).

[Mario Carneiro]

lean4#3184 is step 1 in fixing this