docs for erasing a term / compiling to VM?

Stream: new members

[Joe Glaberman]

Can anybody point me to documentation or a research paper that describes how Lean3 erases a term and then compiles it for execution on the VM? Thanks.

[Joe Glaberman]

Or let me know if the only way to understand how that process works is to study the code...