Exporting all the proof terms

Stream: Is there code for X?

[Michal Buran]

Is there a way to export/print all the proof terms in the current environment?

[Floris van Doorn]

Yes, using metaprogramming. Are you in Lean 3 or in Lean 4? With environment, do you mean the current file, or literally everything that is imported?

[Jason Rute]

I second Foris in asking for more details. But in general it is straightforward to loop through all the proof terms in the environment. See https://github.com/jesse-michael-han/lean-step-public as a repo which does exactly this.

[Jason Rute]

Also see the advice in #metaprogramming / tactics > automatic lemmas retrieval which is a different but similar question.