leanprover-community / leanprover-community/mathlib4
Unused tactic linter fires incorrectly in type ascriptions
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
The following code
import Mathlib
theorem test (A : Set ℕ) (x : ℕ) (hx : x ∈ A) : False := by
have h2 : (Set.nonempty_iff_ne_empty.mpr (by simp : { y : ℕ |
(Set.nonempty_iff_ne_empty.mpr (show A ≠ ∅ from by sorry)).some = y } ≠ ∅)).some = 7 := by
sorry
sorry
triggers the unused tactic linter on the show A ≠ ∅ from by sorry part. Any tactic at all there triggers the same issue. I'm guessing this has something to do with the fact that the tactic is being used to construct a type ascription...? as opposed to the proof term of the theorem itself.
I also started a thread on zulip.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the minimal Lean reproducer in the issue and review the linked Zulip thread for the linter's current behavior. Trace why a tactic inside the type ascription is reported as unused, then verify that the false warning no longer appears while the reproducer still typechecks.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100