Lean private objects

Stream: lean4

[Hanting Zhang]

Is there any documentation on the complex relationships between _cstage1/2, _unsafe_rec, _rarg, _closed, for declarations generated by the Lean compiler? I have a decent idea of what they mean, but are there a set of exact conditions required for the compiler to generate them and specs for how the compiler implicitly references them?

For example, is it always the case that functions that shouldGenerateCode have a corresponding _cstage1/2 object? How is something determined to be _closed?

[Arthur Paulino]

I'm also interested in this :pray: