lean4-htt/src/Init/Data/Iterators
Paul Reichert 7a47bfa208
feat: flatMap iterator combinator (#10728)
This PR introduces the `flatMap` iterator combinator. It also adds
lemmas relating `flatMap` to `toList` and `toArray`.
2025-10-14 12:50:54 +00:00
..
Combinators feat: flatMap iterator combinator (#10728) 2025-10-14 12:50:54 +00:00
Consumers refactor: use Shrink stub in the iterator framework (#10725) 2025-10-14 10:22:14 +00:00
Internal refactor: migrate to new ranges (#8841) 2025-07-07 12:41:53 +00:00
Lemmas feat: flatMap iterator combinator (#10728) 2025-10-14 12:50:54 +00:00
Basic.lean refactor: use Shrink stub in the iterator framework (#10725) 2025-10-14 10:22:14 +00:00
Combinators.lean feat: flatMap iterator combinator (#10728) 2025-10-14 12:50:54 +00:00
Consumers.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Internal.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Lemmas.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
PostconditionMonad.lean feat: flatMap iterator combinator (#10728) 2025-10-14 12:50:54 +00:00
ToIterator.lean refactor: replace some Subarray functions with generic slice functions (#9017) 2025-07-03 19:33:19 +00:00