RFC: Make `Range` behavior "more correct"

Proposal

The following code has "unexpected" output:

def test (n : Nat) : IO Unit :=
  for ii in [0:n:0] do
    IO.print s!"{ii} "

#eval test 10

results in the output

0 0 0 0 0 0 0 0 0 0

Note that here, the 0 step if obvious but it may not always be as clear, since e.g. nat - nat may result in 0.

My proposal would be to make the behavior more in line with e.g. array indexing, e.g. like this:

Local known:

for ii in [0:n:2] do ... -- probably common

Want to make sure it's provably correct:

if h: step > 0 then
    for ii in [0:n:step]'h do ...
else <exception>

I'm just coding, get out of my way:

for ii in [0:n:x-y]! do ... -- I know better

User Experience: How does this feature improve the user experience?
I think this approach eliminates potential errors when using a core component of Lean, and gives the users the tools to choose the "level of correctness" they need when writing said code.

Beneficiaries: Which Lean users and projects benefit most from this feature/change?
I think this would make the "core" more consistent with learner expectations and deliberately chooses familiar syntax used elsewhere.

I am not able to help asses impact on other projects due to my lack of experience, however, here are some stats for the 3-parameter version:

• 4 occurrences in lean4: 3 in code, 1 in tests, all constant values.
• 0 occurrences in baterries
• 0 occurences in mathlib4

I used the following to search:

rg '\[[^:\]]+:[^:\]]+:[^:\]]\]' <dir>

Maintainability: Will this change streamline code maintenance or simplify its structure?
I believe so. Note that given that Mario C. mentioned it was even considered removing the "step" from the available syntax, perhaps the three-parameter version is not that widely used and this change, despite being potentially breaking, could work?

Community Feedback

Zulip

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Note: I am happy to attempt an implementation and submit a PR is there's interest.

Start by reviewing the three-parameter Range syntax and the reported occurrences found with the provided rg search, including the lean4 code and tests. The proposal leaves the intended semantics and implementation choice unresolved; done would require an agreed behavior for zero or nonpositive steps and corresponding validation.