lean4 equivalent of lean3 export of fully elaborated terms

Stream: new members

[John Baker]

lean3 supported a low level export of terms that simplified the task of writing independent term checkers.

It was even baked into the lean executable: lean --export=export.out --recursive

Is there something comparable to this in lean4?

[Mario Carneiro]

https://github.com/leanprover/lean4export

[John Baker]

Thanks