Module emit_lean 

The Lean 4 emitter.

Naturals are Nat, integers Int; machine integers are represented by Nat/Int with explicit range checks that panic! where Rust would panic. Recursion is structural and annotated as such, so the Lean kernel checks termination. Theorems are reconstructed from portable proof plans with Lean tactics and re-checked by the Lean kernel. A JavaScript Number is a Float; the kernel cannot compute with Float, so an assertion about Numbers is checked when main runs, as in the source.

Mirrors js/src/translation/emit-lean.js.

Functions

emit_lean

Emits a checked program as Lean.