Lean 4 equivalent for `#print prefix`

Stream: new members

[Mathieu Guay-Paquet]

Back in Lean 3, I used #print prefix pretty often to explore the codebase. I searched through the docs and skimmed this page with all the interaction commands, but didn't find anything equivalent in Lean 4. Does something like this still exist? (And while we're at it, some others from the old list like #print notation were very useful as well.)

[Kevin Buzzard]

I usually do #check Complex. and then hit ctrl-space to see everything in the Complex namespace

[Aaron Liu]

I think #print prefix still works, but it's very slow for me

[Aaron Liu]

It's in Batteries.Tactic.PrintPrefix