mk: pairlisto — relational zip
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 39s

(pairlisto l1 l2 pairs): pairs is the zipped list of pairs (l1[i] l2[i]).
Recurses on both l1 and l2 in lockstep, building pairs in parallel.

Runs forward, can recover l1 given l2 and pairs, can recover l2 given
l1 and pairs. Different-length lists fail.

5 new tests, 431/431 cumulative.
This commit is contained in:
2026-05-08 11:57:12 +00:00
parent 136cacbd3f
commit c04ddd105b
3 changed files with 50 additions and 0 deletions

View File

@@ -173,6 +173,7 @@ _(none yet)_
_Newest first._
- **2026-05-08** — **pairlisto**: relational zip — pairs is the zipped list of (l1[i] l2[i]). Runs forward, recovers l1 given l2 and pairs, recovers l2 given l1 and pairs. 5 new tests, 431/431 cumulative.
- **2026-05-08** — **iterate-no**: relational iterated application. Applies a 2-arg relation n times (Peano n) starting from x to produce result. Generalises succ-iteration / list-cons-iteration / etc. 4 new tests, 426/426 cumulative.
- **2026-05-08** — **rev-acco / rev-2o**: accumulator-style reversal — faster than appendo-driven reverseo for forward queries because no quadratic appendos. Trade-off: rev-acco is asymmetric (cannot run cleanly backward in run*). 6 new tests, 422/422 cumulative.
- **2026-05-08** — **even-i / odd-i (intarith)**: ground-only parity goals via project. Composes with membero for filtered enumeration: -> . 5 new tests, 416/416 cumulative.