feat: List slices

[datokrat]

This PR introduces slices of lists that are available via slice notation (e.g., xs[1...5]).

• Moved the take combinator and the List iterator producer to Init.
• Introduced a toTake combinator: it.toTake behaves like it, but it has the same type as it.take n. There is a constant cost per iteration compared to it itself.
• Introduced List slices. Their iterators are defined as suffixList.iter.take n for upper-bounded slices and suffixList.iter.toTake for unbounded ones.

Performance characteristics of using the slice list[a...b]:

• when creating it: O(a)
• every iterator step: O(1)
• toList: O(b - a + 1) (given that a <= b)

Because the slice only stores a suffix of xs internally, two slices can be equal even though the underlying lists differ in an irrelevant prefix. Because the stop field is allowed to be beyond the list's upper bound, the slices [1][0...1] and [1][0...2] are not equal, even though they effectively cover the same range of the same list. Improving this would require us to call List.length when building the slice, which would iterate through the whole list.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-30 14:26:59)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-13 09:55:18)
• 🟡 Reference manual branch lean-pr-testing-11019 build against this PR didn't complete normally. (2025-11-13 13:50:53) View Log
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-14 11:17:14)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-11019 built against this PR, but testing failed. (2025-10-30 15:51:55) View Log
• ❌ Mathlib branch lean-pr-testing-11019 built against this PR, but testing failed. (2025-10-31 16:44:44) View Log
• ✅ Mathlib branch lean-pr-testing-11019 has successfully built against this PR. (2025-11-01 12:04:41) View Log
• ✅ Mathlib branch lean-pr-testing-11019 has successfully built against this PR. (2025-11-11 09:48:16) View Log
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-11-13 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-11-13 09:55:17)
• ✅ Mathlib branch lean-pr-testing-11019 has successfully built against this PR. (2025-11-13 15:07:41) View Log
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-11-14 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-11-14 11:17:13)

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 7cba2da against ed73cdd are in! @datokrat

Runs (1)

• other exited with code 1 (🟥)

Major changes (1)

• stdlib//number of imported bytes changed by +1.5% (🟥).

Minor changes (3)

• stdlib//instructions changed by +0.2% (🟥).
• stdlib//number of imported consts changed by +1.2% (🟥).
• stdlib//number of imported entries changed by +0.9% (🟥).

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 10bb408 against 2b85e29 are in! @datokrat

Runs (1)

• other exited with code 1 (🟥)

Major changes (1)

• stdlib//number of imported bytes changed by +1.6% (🟥).

Minor changes (3)

• stdlib//instructions changed by +0.2% (🟥).
• stdlib//number of imported consts changed by +1.3% (🟥).
• stdlib//number of imported entries changed by +0.9% (🟥).

[datokrat]

!radar

[leanprover-radar]

Benchmark results for ac54c21 against de07370 are in! @datokrat

Minor changes (7)

• iterators (elab)//instructions changed by +0.7% (🟥).
• lake build clean//instructions changed by +0.8% (🟥).
• language server startup//instructions changed by +0.7% (🟥).
• stdlib//instructions changed by +0.2% (🟥).
• stdlib//number of imported bytes changed by +0.9% (🟥).
• stdlib//number of imported consts changed by +0.5% (🟥).
• workspaceSymbols with new ranges//instructions changed by -3.0% (✅).

[datokrat]

!radar

[leanprover-radar]

Benchmark results for ac54c21 against de07370 are in! @datokrat

Minor changes (7)

• iterators (elab)//instructions changed by +0.7% (🟥).
• lake build clean//instructions changed by +0.8% (🟥).
• language server startup//instructions changed by +0.7% (🟥).
• stdlib//instructions changed by +0.2% (🟥).
• stdlib//number of imported bytes changed by +0.9% (🟥).
• stdlib//number of imported consts changed by +0.5% (🟥).
• workspaceSymbols with new ranges//instructions changed by -3.0% (✅).