nx_theorem_registry_test.nx
buildroot/runtime/nx_theorem_registry_test.nx
about
nx_theorem_registry_test.nx -- smoke for the L0->L2.5 bulk registry.
Loads the 42k+ mathlib4 shard and verifies:
- n_records >= 10000 (rock-solid threshold)
- lookup by name works (sample known theorem)
- kind aggregates are non-zero
- source aggregates show all lean
dependencies 5 imports · 0 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_theorem_registry.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 15 | const NX_THM_T_THRESHOLD: nx_int = 10000 |
functions
| 17 | func main() -> nx_exit |