Module export 

Reading a lean4export NDJSON stream straight into the kernel core.

The export is already a maximally shared DAG: every name, level and expression is a numbered record defined before it is used. Each record becomes one interned node, so the export’s sharing is preserved exactly and nothing is ever expanded into a tree. Declarations are checked the moment they arrive; nothing of the input is retained but the interned DAG.

Structs

Observe

How a run is observed, beside the kernel’s own configuration.

Reader

Stats

Enums

Verdict

The verdict of checking one export, in the Arena’s exit-code protocol.

Traits

DeclMeter

Observes each declaration the reader hands to the kernel: begin just before the kernel checks it and end just after, with its name, its record kind and whether it was admitted. A measurement hook; checking never depends on it.

Functions

check_export

Checks a whole export stream.

check_export_in

Checks a whole export into the caller’s kernel, which keeps everything admitted — a command that exits once it has reported need never pay for tearing the kernel down.

check_export_observed

check_export_sized, observed as observe asks.

check_export_sized

check_export_with for an input whose size is known, so the stores are sized once.

check_export_with

Checks a whole export with a kernel configured by configure first.

load_refs

Loads a file of named reference terms into k’s store.