Regex matcher in lean 4 via brzozowski derivatives, with correctness established against an inductive match relation
Updated 2026-01-07 19:03:05 +00:00