linter.unusedSimpArgs

Stream: mathlib4

[Kenny Lau]

I think the unused simp args linter should only activate when the goal has been cleared.

[Kenny Lau]

#mwe :

import Mathlib.Data.Nat.Basic

def addOne (n : ℕ) : ℕ := n + 1
def addTwo (n : ℕ) : ℕ := n + 2

lemma addOne_eq_add_one (n : ℕ) : id (addOne n) = n + 1 := by
  simp [id, addTwo] -- linter activates but shouldn't

lemma addOne_eq_add_one' (n : ℕ) : id (addOne n) = n + 1 := by
  simp [id, addOne, addTwo] -- linter correctly activates

[Eric Wieser]

I think it's pretty useful to know immediately that a simp lemma didn't fire when you expected it to

[Damiano Testa]

I agree with Eric: knowing which lemmas you thought would apply, but didn't, can be useful to figure out what is going on.

[Kenny Lau]

fair point