v4.26.0-rc2

[pandaman64]

Note

Migrates the regex engine and public API from Iterator/Substring to ValidPos/Slice, refactors backtracker/VM and proofs to BVPos-based semantics, updates docs/tests, and bumps Lean/mathlib to v4.26.0-rc2.

• Core/API:
  • Replace Iterator/Substring with ValidPos/Slice across Regex API (find, matches, captures, transform, split, etc.).
  • Introduce Regex.Data.BVPos and parameterize CapturedGroups/Strategy updates by string.
• Backtracker/VM:
  • Refactor traversal (captureNext, pushNext, eachStepChar, εClosure) to BVPos; simplify/rename invariants.
  • Update anchors/char/sparse handling to use ValidPos getters and end checks.
• Semantics/Proofs:
  • Port NFA step/closure/path lemmas to ValidPos/BVPos; remove BoundedIterator proofs.
  • Adapt equivalence/refinement and compile correctness to new types.
• Docs/Examples:
  • README and example code updated to new Slice-based API and outputs.
• Tests:
  • Adjust expectations to Slice and position fields; add helpers; keep behavior parity.
• Tooling:
  • Bump Lean/toolchain and deps (mathlib/proofwidgets/etc.) to v4.26.0-rc2.

^{Written by Cursor Bugbot for commit e13757d. This will update automatically on new commits. Configure here.}

[cursor]

This PR is being reviewed by Cursor Bugbot

Details

You are on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle.

To receive Bugbot reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.