nx_rewrite.nx
buildroot/runtime/nx_rewrite.nx
about
nx_rewrite.nx -- equational normaliser engine.
Closes "no equational rewriter" gap. HOL Light has REWRITE_TAC,
Coq has rewrite, Lean has simp. Ours emits v2-kernel-checked
rewrite steps using the existing EQ_SYM / EQ_TRANS rules + a
substitution helper.
Strategy: leftmost-outermost. Given a Term `goal` and a set of
orientation-tagged equations [(lhs == rhs)...], walk the term and
apply the first matching rewrite at each position, emitting an
EQ_TRANS chain. Bounded iterations to guarantee termination.
dependencies 1 imports · 1 importers
imports: nx_kernel_v2.nx
imported by: nx_world_class_test.nx
structs
| none |
consts
| 21 | const NX_REWRITE_MAX_ITER: nx_int = 32 |
functions
| 30 | func nx_rewrite_step(ch: *K2Chain, eqs: *nx_int, n_eqs: nx_int, current: *Term) -> nx_int |
| 55 | func nx_rewrite_normalise(ch: *K2Chain, eqs: *nx_int, n_eqs: nx_int, start: *Term) -> nx_int |