code wiki / (root) / nx_mizar_stream_ingest.nx

nx_mizar_stream_ingest.nx

buildroot/runtime/nx_mizar_stream_ingest.nx

3633 B110 linesdepth 7pulls 18 transitivereach 2 importersview sourcekind librarytopic mizar
docsdependenciesstructsconstsfunctions

about

nx_mizar_stream_ingest.nx -- Mizar parser -> 5-defense runner. Synthesizes the canonical MML key "<ARTICLE>:th <N>" so dedup works despite Mizar's multi-field identity (article, number, label). genealogy_id: mizar_to_qed_2026 + ingest_runner_composition lineage_id: source_adapter_multi_field_key

dependencies 5 imports · 2 importers

nx_syscalls.nx nx_tier.nx nx_strconv.nx nx_mizar_ingest.nx nx_ingest_runner.nx nx_mizar_stream_ingest.nx nx_mizar_dir_ingest.nx nx_mizar_stream_ingest_test.nx

imports: nx_syscalls.nxnx_tier.nxnx_strconv.nxnx_mizar_ingest.nxnx_ingest_runner.nx

imported by: nx_mizar_dir_ingest.nxnx_mizar_stream_ingest_test.nx

structs

none

consts

none

functions

21func nx_miz_strlen(s: *u8) -> nx_size
27func nx_miz_str_copy(dst: *u8, off: nx_size, src: *u8) -> nx_size
36func nx_miz_kind_tag(kind: nx_int, out: *u8) -> nx_size
called by 1: nx_miz_key_build
45func nx_miz_key_build(d: *MizarDecl, key_out: *u8) -> nx_size
65func nx_miz_row_build(d: *MizarDecl, out: *u8) -> nx_size
92func nx_mizar_stream_offer_all(