nx_triangulation_algebra.nx
buildroot/runtime/nx_triangulation_algebra.nx
about
nx_triangulation_algebra.nx -- L5 verification of algebraic
properties that nx_int satisfies.
Each property tested here is shared with MANY mathlib4 / Coq / HOL
theorems by name pattern: add_comm, mul_assoc, mul_zero, etc.
When the substrate proves the property for nx_int across multiple
sample inputs, it gives an L5 verdict that AUTHORIZES the shape-
matching theorems in the QED corpus to claim PROVED-on-nx_int.
This is not Lean transpilation -- it's an honest substrate-side
proof that the SAME ALGEBRAIC IDENTITIES hold in NishiLang.
dependencies 3 imports · 0 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.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
| none |
functions
| 23 | func nx_check_prop(label: *u8, ok: nx_int, agree: *nx_int, fail: *nx_int) |
| 34 | func main() -> nx_exit |