feat: new, continuation-based, repeat loop with verification potential

[Rob23oba]

(experiment) Implementation of repeatNew from #13209 (comment)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3770b3dcb8b1b3340e0252760dc68e8e61daef06 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-04 11:35:25)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3770b3dcb8b1b3340e0252760dc68e8e61daef06 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-04 11:35:26)

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 0393f05 against 3770b3d are in. Significant changes detected! @Rob23oba

• ✅ build//instructions: -1.5G (-0.01%)

Medium changes (1✅)

• ✅ build/module/Lean.Meta.Tactic.Grind.AC.Eq//instructions: -1.2G (-3.41%) (reduced significance based on absolute threshold)

Small changes (45✅, 12🟥)

Too many entries to display here. View the full report on radar instead.