nx_world_class_test.nx
buildroot/runtime/nx_world_class_test.nx
about
nx_world_class_test.nx -- prove every named blocker is gone.
One smoke that exercises arith / classical / tactics / rewriter /
emitter end-to-end via v2 kernel. Per user 2026-05-15: "no losses".
Each test gets an assertion number; main() returns it on first
failure (per nx_smoke_lib.sh convention). Returns 0 only when all
pass.
dependencies 6 imports · 0 importers
imports: nx_tactics.nxnx_arith.nxnx_classical.nxnx_proof_emit.nxnx_rewrite.nxnx_probability.nx
imported by: nobody (leaf or entry point)
structs
| none |
consts
| 17 | const SYM_A: nx_int = 1001 |
| 18 | const SYM_B: nx_int = 1002 |
| 19 | const SYM_P: nx_int = 1100 |
functions
| 21 | func one_axiom(a: nx_int) -> *nx_int |
| 27 | func two_axioms(a: nx_int, b: nx_int) -> *nx_int |
| 35 | func t1_nat_literal() -> nx_int |
| 50 | func t2_peano_axioms() -> nx_int |
| 64 | func t3_finite_induction() -> nx_int |
| 94 | func t4_classical_lem() -> nx_int |
| 110 | func t5_classical_other() -> nx_int |
| 124 | func t6_rewriter() -> nx_int |
| 149 | func t7_tactics() -> nx_int |
| 166 | func t8_emit() -> nx_int |
| 178 | func t9_probability() -> nx_int |
| 202 | func main() -> nx_exit |