What a user's package gets from import Lean2Js #

What a user's package gets from import Lean2Js: the subset, the reference semantics, the compiler, and emit.

The proofs about the compiler are not here. They are Lean2Js/Checks.lean, which this repository's CI builds and a user never imports — re-checking them costs a user 98 MB of olean and tells them nothing their own build could not already assume.