Module emit_javascript 

The JavaScript emitter: writes a checked program as a strict ES module with its translation contract.

Every portable integer is a BigInt, so naturals and integers stay unbounded and machine integers are range-checked exactly as Rust checks them; a Number stays a Number. Data values are plain objects whose $ property names the constructor. Modules become object literals referenced by qualified names. Theorems cannot be proved in JavaScript: each becomes an executable property, checked over a bounded domain by --ml-check-theorems, while the proof obligation stays discharged by the source language’s kernel.

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

Functions

emit_javascript

Emits a checked program as JavaScript.