While loop - #184

Draft

crei wants to merge 24 commits into

origin_mainfrom

Commits on Aug 31, 2026

chore: bump mathlib to e06eff5, fix breaking changes (#848)

mathlib-nightly-testing[bot]
and
chenson2018
authored
21ed7bd

Commits on Sep 1, 2026

chore: document two heavy grind uses (#850)
jessealama
authored
daedb5e
chore(LTS/MapHom): golf mapHom_mTr proof (#849)
jessealama
authored
aeb2e41
chore(HML/LogicalEquivalence): golf to remove `mergeWithGrind` opt (#851)
jessealama
authored
bba5e73

Commits on Sep 2, 2026

Commits on Sep 3, 2026

Add two examples.
crei
committed
5330b08
Merge remote-tracking branch 'self/tm_finite' into tm_finite
crei
committed
bc1122a
Update wording.
crei
committed
1927c42

Commits on Sep 4, 2026

Extend result to "almost constant" functions.
crei
committed
eae0622

Commits on Sep 5, 2026

feat(Turing): while/loop combinators, plumbing and encoding requirements

crei
and
Copilot
committed
e4c6bfb
feat(Turing): prove the loop combinator

crei
and
claude
committed
fa21954

Commits on Sep 8, 2026

feat(Turing): factor the conditional through the recursor of `Bool`

crei
and
claude
committed
ecd9e67
feat(Turing): the generic constructor of a non-recursive inductive type

crei
and
claude
committed
3f5e73c
feat(Turing): requirements on a pair encoding, as complexities only

crei
and
claude
committed
fd2051a
test(Turing): a type with two constructors of arity two

crei
and
claude
committed
2449092
refactor(Turing): make the finite case analysis the primitive

crei
and
claude
committed
552f510
refactor(Turing): one bound for the scrutinee and every branch

crei
and
claude
committed
b20a39c
docs(Turing): note that `_match`'s `f` is inferred from the goal

crei
and
claude
committed
3860f30
test(Turing): destructuring matches, with and without junk

crei
and
claude
committed
1af43a7
test(Turing): match on `Span` itself rather than on a computed scrutinee

crei
and
claude
committed
0a461cc
feat(Turing): `_match` needs a finite range, not a finite scrutinee type

crei
and
claude
committed
9413495
refactor(Turing): plumbing postconditions as vector equalities

crei
and
claude
committed
2b60af8
refactor(Turing): extract the loop proof's reusable parts

crei
and
claude
committed
e76bda0