simp? suggests generated equations lemma names

[nomeata]

Consider this:

import Std

def foo : Nat → Nat 
  | 0 => 0
  | n+1 => foo n
decreasing_by decreasing_tactic

def foo2 : foo 2 = 0 := by
  simp? [foo]
  -- suggests: simp only [foo._eq_2, foo._eq_1]
  -- but that yields: unknown constant 'foo._eq_2'

These foo._eq_6 lemmas are created on demand when you use simp [foo] or rw [foo]; from then on they are available. But if you just mention them manually like this, they may not exist yet.

Therefore, simp? should not suggest them. Instead it should suggest simp only [foo].

Versions

4.6.0 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.