simp only version complaining about unused lemmas

Stream: lean4

[Michael Rothgang]

Is there a way to make simp complain if it cannot use a given lemma?

(I'm generalising lemmas from one typeclass to a more general one, and have to debug quite a few simp calls which fail - as some used lemma has not been generalised yet. Squeezing the simp (before my change) shows which lemmas were used, but does not tell me which ones did not apply. A mode of simp only to complain "I could not use this lemma" would be rather helpful.

[Michael Rothgang]

Right now, my best workaround is to split the call into simp only [lemma1]; simp only [lemma2]` and see which ones make no progress.

[Jovan Gerbscheid]

(deleted)

[Jovan Gerbscheid]

My approach would be to replace simp only with simp? only and compare the result

[Ruben Van de Velde]

The output order of simp? is pretty stable now, so often you can replace its output with simp_rw

[Michael Rothgang]

Thank you, both, for the tricks!