Unfolding local definitions

Stream: general

[Alex J. Best]

@Meow|566171 Can you move this to another thread? It seems unrelated to this one (simply edit your message).
@Martin Dvořák what do you not like about it?

[Notification Bot]

4 messages were moved here from #general > Please stop adding generalized API around coercions by Anne Baanen.

[Martin Dvořák]

It doesn't allow me to specify what exactly I want to unfold. However, we don't have to talk about it again. In the end change saves me usually.

[Alex J. Best]

Can you link to a MWE or when you last talked about it?

[Meow]

Alex J. Best said:

@Meow|566171 Can you move this to another thread? It seems unrelated to this one (simply edit your message).
Martin Dvořák what do you not like about it?

Sorry, I'm not familiar to Zulip and know how to change the thread of a posted message just now.

[Martin Dvořák]

Don't worry. It has already been moved.

[Moritz Doll]

Meow said:

What is the best way to unfold local definitions?

You can use rw with the definition, dunfold, dsimp or just use apply, refine or exact directly since they (mostly) don't care about definitional equality