Extract proof script with metaprogramming

Stream: lean4

[Adam Topaz]

I would like to have some method of extracting the proof script used to prove a lemma (assuming it was proved using tactics), say with a given name `name, in some way. Unfortunately, I don't even know where to start. Is this possible to do with metaprogramming somehow? I thought that this was discussed at some point recently, but I can't seem to find this discussion.

[Sebastian Ullrich]

The input syntax is discarded after elaboration, you would have to drive processing of the file yourself like how LeanInk does it

[Adam Topaz]

Ah! Good point! I didn't think about looking at leanink. I will do that, thanks!