feat: Std.Iterators bridge with LawfulParserStream and WF recursion for folds#97

Open

NicolasRouquette wants to merge 3 commits into

fgdorais:mainfrom

NicolasRouquette:std-iterators

Commits on Feb 22, 2026

feat: add Std.Iterators bridge and make fold combinators total
NicolasRouquette
committed
feat: add LawfulParserStream, fix sorry, replace fuel with WF recursion
NicolasRouquette
committed

Commits on Feb 26, 2026

feat: add fold-combinator specification lemmas for m=Id\n\nAdd upstream lemmas in lean4-parser that make the fold-based\nparser combinators deductively transparent for proofs:\n\n- efoldlPAux_eq: o…
NicolasRouquette
committed