code wiki / (root) / nx_kernel_v2_discharge_test.nx

nx_kernel_v2_discharge_test.nx

buildroot/runtime/nx_kernel_v2_discharge_test.nx

8448 B152 linesdepth 6pulls 6 transitivereach 0 importersview sourcekind gate/prooftopic kernel
docsdependenciesstructsconstsfunctions

about

nx_kernel_v2_discharge_test.nx -- ASSUMPTION + IMP_INTRO + NOT_INTRO + OR_INTRO + EQ_SYM + EQ_TRANS exercises. These rules are what turn the kernel from "stops at contradiction" to "produces real theorems".

dependencies 4 imports · 0 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_kernel_v2.nx nx_kernel_v2_discharge_test.nx

imports: nx_syscalls.nxnx_runtime.nxnx_tier.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

main println sys_write strlen sys_mmap nx_k2_chain_new sys_mmap ↻ nx_term_const sys_mmap ↻ nx_k2_assume nx_k2_at nx_k2_hyps_alloc sys_mmap ↻ nx_k2_hyps_copy_in nx_k2_hyps_at nx_k2_imp_intro nx_k2_at ↻ sys_mmap ↻ nx_k2_hyps_remove nx_k2_hyps_at ↻ nx_term_eq nx_term_eq ↻ nx_term_arg nx_k2_hyps_alloc ↻ nx_k2_hyps_copy_in ↻ nx_k2_imp sys_mmap ↻ nx_term_app sys_mmap ↻ nx_k2_at ↻ nx_k2_mark_theorem nx_k2_at ↻ nx_k2_imp ↻ nx_k2_not sys_mmap ↻ nx_term_app ↻ nx_k2_axiom nx_k2_at ↻ nx_k2_modus_ponens nx_k2_at ↻

structs

none

consts

12const SYM_P: nx_int = 1001
13const SYM_Q: nx_int = 1002
14const SYM_A: nx_int = 1100
15const SYM_B: nx_int = 1101
16const SYM_C: nx_int = 1102

functions

18func main() -> nx_exit {
calls 18: printlnnx_k2_chain_newnx_term_constnx_k2_assumenx_k2_imp_intronx_k2_at+12