lean4-htt/src/Init/Data/Iterators
Paul Reichert 83e226204d
feat: introduce slices (#8947)
This PR introduces polymorphic slices in their most basic form. They
come with a notation similar to the new range notation. `Subarray` is
now also a slice and can produce an iterator now. It is intended to
migrate more operations of `Subarray` to the `Slice` wrapper type to
make them available for slices of other types, too.

The PR also moves the `filterMap` combinators into `Init` because they
are used internally to implement iterators on array slices.
2025-06-26 15:29:03 +00:00
..
Combinators feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
Consumers feat: polymorphic ranges (#8784) 2025-06-26 08:18:11 +00:00
Internal refactor: partially move iterators to Init (#8767) 2025-06-18 10:08:04 +00:00
Lemmas feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
Basic.lean feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
Combinators.lean feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
Consumers.lean refactor: partially move iterators to Init (#8767) 2025-06-18 10:08:04 +00:00
Internal.lean refactor: partially move iterators to Init (#8767) 2025-06-18 10:08:04 +00:00
Lemmas.lean feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
PostconditionMonad.lean feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00
ToIterator.lean feat: introduce slices (#8947) 2025-06-26 15:29:03 +00:00