Weird forIn and Range behaviour.

[grhkm21]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This is more like a question or confirmation request. I noticed that inside a Id.run monad, if I iterate through a Std.Range object with step := 0, for example [0 : 10 : 0] representing { start := 0, stop := 10, step := 0 }, it executes the code 10 times instead of doing nothing. It felt unintuitive to me and I wanted to confirm if this should be intended behaviour.

I also briefly read through the original paper on do, but it doesn't seem to mention anything about it.

Also sorry in advance if some terminology is incorrect, I just started learning Lean 4 a few days ago.

Steps to Reproduce

Run the following code:

def f := Id.run do
  let mut r := 0
  for _ in [0 : 10 : 0] do
    r ← r + 1
  return r

-- 10
#eval f

I expected to see 0 (NOP) as the result, which is the default for many undefined behaviours e.g. 1 / 0 = 0. but instead it runs the loop 10 times. To be more clear,

def f := Id.run do
  let mut r := #[]
  for i in [0 : 10 : 0] do
    r ← r.append #[i]
  return r

-- #[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
#eval f

Which shows that the loop iterates the variable i 10 times, but I will expect it to run 0 times and return #[].

Versions

Shouldn't matter but Lean (version 4.0.0-nightly-2023-02-23, commit 3f6c5f17db30, Release).

[Kha]

Related: #1962

[grhkm21]

I assume this can be closed since the API of Range has changed drastically (I heard). Feel free to re-open if that's not the case.