Module output 

Output and aborts as values, for the targets whose programs are pure.

Rust and JavaScript print where the source prints and abort where it aborts; in Lean and Rocq a function that prints or may abort, directly or through a function it calls, takes the lines printed before it and returns them, with the lines it prints added in front, paired with its value, or, when it aborts, with the source’s abort message instead of a value; main prints the lines each of its steps adds and stops with the message of the first abort. The rewriting is target-independent: it yields a portable-core program without print and abort nodes, machine-integer arithmetic or checked conversions, whose pairs are generated data types.

Mirrors js/src/translation/output.js.

Functions

thread_output

The checked program with its output and aborts threaded through, or the program itself when nothing below main prints or aborts.