feat: introduce slices

[datokrat]

trafficstars

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.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-25 09:08:57) Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 40d2c9946319716228b414e501e71b7f959e1619 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. (2025-06-26 11:40:19)
• 💥 Mathlib branch lean-pr-testing-8947 build failed against this PR. (2025-06-26 11:43:34) View Log
• ✅ Mathlib branch lean-pr-testing-8947 has successfully built against this PR. (2025-06-26 15:22:53) View Log

[datokrat]

@david-christiansen I think you are being notified because you are the code owner of Subarray. Here's some context: I am migrating Subarray to a more polymorphic setting. This required me to replace the definition of Subarray. However, I am keeping its whole public API except for low-level details (e.g. the constructor). Not many things broke besides Subarray.lean and Subarray/Split.lean While fixing some compile errors in Split.lean, I also implemented split in terms of take and drop. Feel free to leave comments if you think that things could be improved!

[david-christiansen]

It all looks good to me :)