code wiki / (root) / nx_hol_stream_ingest.nx

nx_hol_stream_ingest.nx

buildroot/runtime/nx_hol_stream_ingest.nx

1934 B65 linesdepth 7pulls 18 transitivereach 2 importersview sourcekind librarytopic hol
docsdependenciesstructsconstsfunctions

about

nx_hol_stream_ingest.nx -- HOL Light parser -> 5-defense runner. Output JSONL row: {"source":"hol","kind":N,"name":"..."} genealogy_id: hol_light_to_qed_2026 + ingest_runner_composition lineage_id: source_adapter

dependencies 4 imports · 2 importers

nx_syscalls.nx nx_tier.nx nx_hol_ingest.nx nx_ingest_runner.nx nx_hol_stream_ingest.nx nx_hol_dir_ingest.nx nx_hol_stream_ingest_test.nx

imports: nx_syscalls.nxnx_tier.nxnx_hol_ingest.nxnx_ingest_runner.nx

imported by: nx_hol_dir_ingest.nxnx_hol_stream_ingest_test.nx

structs

none

consts

none

functions

19func nx_hol_strlen(s: *u8) -> nx_size
25func nx_hol_str_copy(dst: *u8, off: nx_size, src: *u8) -> nx_size
called by 1: nx_hol_row_build
34func nx_hol_row_build(d: *HolDecl, out: *u8) -> nx_size
48func nx_hol_stream_offer_all(