Module emit_common 

State shared by the emitters.

The state holds target names for every declaration, the source-to-target mapping, and the encodings and assumptions a translation relies on. Every emitter records what it did here, so the translation contract lists exactly the choices that were made for this program.

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

Structs

Assumption

An assumption the translation relies on, with the program-specific details.

AssumptionText

A fixed assumption text, so that contracts compare across runtimes.

Dependence

Whether a node depends on declarations of a kind, directly or not.

EmitOptions

Target naming rules for EmitState.

EmitState

Emitted

An emitted target program together with its translation contract.

Encoding

A representation choice the translation made.

Mapping

Where a source declaration went in the target.

TheoremRecord

A theorem or assertion the target states, and how it is discharged.

Enums

CtorStyle

How constructors are named: inside a module next to their type (Rocq), or under the type.

Constants

IN_BOUNDS_READS

Functions

dependencies

Declarations every declaration refers to (types, functions, constructors, lemmas).

mutual_groups

Each function the checker marked mutual, mapped to its group.

order_declarations

Declarations in an order where each follows everything it uses.

unthreaded

An operation that may abort, which output threads as a value before a pure target sees it.