Have #print unfold definitions?

Stream: lean4

[Asta Halkjær From]

I have a definition that builds an inhabitant of an inductive type using several helper definitions that abbreviate smaller parts.
This means that when I #print my definition, those helper definitions show up in the output.
I would like to have them all unfolded down to the constructors of the inductive type, so I can see the full unabbreviated term.
Can I do this?

[Sebastian Ullrich]

#reduce does this, though it will also continue inside the constructor arguments of your inductive type, which for the non-recursive arguments sometimes can be more than you wished for.

[Asta Halkjær From]

Perfect! I knew I was missing something...