nx_kernel_v2_test.nx
buildroot/runtime/nx_kernel_v2_test.nx
about
nx_kernel_v2_test.nx -- exercise the semantic kernel.
Three scenarios:
T1. Valid modus ponens chain -- kernel accepts.
T2. Modus ponens with MISMATCHED antecedent -- kernel REJECTS.
This is the test that distinguishes a real kernel from a
rubber stamp. HOL Light, Coq, Lean all reject this; the
v1 (structural) kernel would not.
T3. AND-intro then AND-elim_L round-trip -- kernel preserves
the formula structure.
dependencies 5 imports · 0 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_unify.nxnx_kernel_v2.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
| 19 | const SYM_P: nx_int = 1001 |
| 20 | const SYM_Q: nx_int = 1002 |
| 21 | const SYM_R: nx_int = 1003 |
| 22 | const SYM_A: nx_int = 1004 |
functions
| 24 | func main() -> nx_exit |