nx_proof_emit.nx
buildroot/runtime/nx_proof_emit.nx
about
nx_proof_emit.nx -- two-column proof emitter.
Closes the named blocker for "two-column proof" -- previously
DERIVABLE but not yet shipped as a callable engine. This file
makes it L3 (callable) per the every-primitive-usable cardinal.
Walks a v2 chain and prints each step in the standard math two-
column form:
#idx | statement | justification
-----+------------------------+--------------------------------
0 | A | AXIOM
1 | A => B | AXIOM
2 | B | MODUS_PONENS (1, 0)
This is the format every K-12 / undergrad textbook uses for proofs.
HOL Light has it via print_thm; Coq / Lean have similar.
dependencies 1 imports · 2 importers
imports: nx_kernel_v2.nx
imported by: nx_world_class_test.nxnx_world_demo_test.nx
structs
| none |
consts
| none |
functions
| 28 | func nx_emit_rule_name(rule: nx_int) -> nx_int called by 1: nx_emit_two_column |
| 51 | func nx_emit_term(t: *Term) -> nx_int called by 4: nx_emit_termnx_emit_two_columndemo1_deriv_x3demo9_prob calls 2: nx_emit_termnx_term_arg |
| 102 | func nx_emit_premises(t: *K2Thm) -> nx_int called by 1: nx_emit_two_column |
| 117 | func nx_emit_two_column(ch: *K2Chain) -> nx_int |