unfold tactic without requiring names

Stream: Is there code for X?

[Kayla Thomas]

Is there an unfold tactic that does not require supplying the names of the definitions to unfold?

[Kayla Thomas]

Is this one of the configuration options to simp?

[Kyle Miller]

In Lean 3 you can do simp! to get it to unfold definitions, and this is short for simp {iota_eqn := tt}. There's a little about it here

[Kayla Thomas]

Thank you. Is there a way to make simp only unfold definitions and list the names of the definitions it unfolded (like squeeze_simp, but for only doing what dunfold or unfold does)?

[Scott Morrison]

I don't think so. I'm tempted to suggest that this is probably the wrong thing to want in the first place. :-) It takes a bit of getting used to the idea, but usually we want to avoid unfolding definitions as much as possible! Perhaps you could #xy and explain the situation where you'd like to have this sort of automatic unfolding?