Module emit_rocq 

The Rocq emitter: writes a checked program as Rocq with its translation contract.

Naturals become binary N and integers Z, so programs run at their source sizes (unary nat cannot hold 20!). Structural recursion over data is a Fixpoint; recursion that decreases a natural is a Function with the measure N.to_nat, whose obligations lia discharges and whose equation lemma the reconstructed proofs rewrite with. A JavaScript Number is a primitive float, which the kernel computes with, so assertions about Numbers are still theorems closed by computation.

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

Constants

FLOAT_PRELUDE

The Require lines of a file that uses Numbers. Number literals are written as in the source; Rocq reads each one as the nearest float, as JavaScript does, and would otherwise warn that it rounds.

ROCQ_PRELUDE

The Require lines every emitted file starts with.

Functions

emit_rocq

Emits a checked program as Rocq.