`proof_wanted` is linted for unused arguments

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

234 stars 98 forks source link

`proof_wanted` is linted for unused arguments #938

Open YaelDillies opened 2 weeks ago

YaelDillies commented 2 weeks ago

We should disable the unused argument linter and the new variable inclusion mechanism linter in proof_wanted. Currently, we have the following behavior:

import Batteries.Util.ProofWanted

class Foo where

variable [Foo]

proof_wanted two_eq_two (h : 1 + 1 = 2) : 2 = 2
/-
unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`

included section variable '[Foo]' is not used in 'two_eq_two', consider excluding it
-/

digama0 commented 2 weeks ago

The section variable linter is not disableable, this issue is not actionable until that changes.

YaelDillies commented 2 weeks ago

See https://github.com/leanprover/lean4/pull/5036