Iteration-totality story
Priority: P2 — Medium-term
Structural + Int-bounded total recursion with enforced non-negativity.
AILang's iteration story stays as-is (structural / tail recursion; tail-app intact). The genuine ambition — make f(n-1)-family recursion (incl. branching tree builders) total by construction with the non-negative-entry precondition enforced, not merely documented — is deferred here because doing it without a purity-pillar concession requires refinement/Nat type machinery the language has not built (Decision 4 keeps refinements opaque, no SMT). Not abandoned; correctly sequenced after the type machinery.
depends on: a future Nat/refinement-types milestone (no spec yet).
context: docs/specs/0032-iteration-discipline-revert.md (why the 2026-05 attempt was reverted); the branching-builder counter-example that surfaced the gap landed in the it.3 iter commit.
No results
Try adjusting your search filters.