tactic for extracting the current tactic state into theorem

Stream: general

[Frederick Pu]

is there a tactic for automatically extracting the current tactic state into a theorem declaration?

[Damiano Testa]

There is extract_goal, but a code-action for creating a stand-alone declaration has not yet been written.

[Frederick Pu]

on similar note is there good way making lean metaprogram that takes a lean file and inlines all the theorems except the last theorem as a have statements in the last theorem

[Matt Diamond]

I don't have the answer but that sounds like a metaprogram that does the exact opposite of what people normally advise... what's the use case?