feat: polymorphic ranges

[datokrat]

This PR introduces ranges that are polymorphic, in contrast to the existing Std.Range which only supports natural numbers.

Breakdown of core changes:

• Lean.Parser.Basic: Modified the number parser (Lean.Parser.Basic) so that it will only consider a single dot to be part of a decimal number. 1.. will no longer be parsed as 1. followed by ., but as 1 followed by ...
• The test ellipsisProjIssue ensures that #check Nat.add ...succ produces a syntax error. After introducing the new range notation (see below), it returns a different (less nice) error message. I updated the test to reflect the new error message. (The error message will become nicer as soon as a delaborator for the ranges is implemented. This is out of scope for this PR.)

Breakdown of standard library changes:

Modified modules: Init.Data.Range.Polymorphic (added), Init.Data.Iterators, Std.Data.Iterators

• Introduced the type Std.PRange that is parameterized over the type in which the range operates and the shapes of the lower and upper bound.
• Introduced a new notation for ranges. Examples for this notation are: 1...*, 1...=3, 1...<3, 1<...=2, *...=3.
• Defined lots of typeclasses for different capabilities of ranges, depending on their shape and underlying type.
• Introduced Iter(M).size.
• Introduced the Iter(M).stepSize n combinator, which iterates over an iterator with the given step size n. It will drop n - 1 values between every value it emits.
• Replaced LawfulPureIterator with a new and better typeclass LawfulDeterministicIterator.
• Simplified some lemma statements in the iterator library such as IterM.toList_eq_match, which unnecessarily matched over a Subtype, hindering rewrites due to type dependencies.

Reasons for the concrete choice of notation:

• lean4-cli uses ...-based notation for the Cmd notation and it clashes with ...a range notation.
• test 2461 fails when using two-dot-based notation because of the existing { a.. } notation.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86eded35db40fadcd718eed738e0860b942841b1 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-23 08:44:03)
• ✅ Mathlib branch lean-pr-testing-8784 has successfully built against this PR. (2025-06-23 10:02:06) View Log
• ✅ Mathlib branch lean-pr-testing-8784 has successfully built against this PR. (2025-06-23 14:01:22) View Log
• ✅ Mathlib branch lean-pr-testing-8784 has successfully built against this PR. (2025-06-23 22:30:02) View Log
• ❗ 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 08:37:42)

[TwoFX]

Excellent work.