range with step

Stream: Is there code for X?

[Diana Kalinichenko]

Is there something in mathlib that generates a list of numbers x, x + n, x + 2n, ... up to a maximum m like list(range(x, m, n)) in Python?

[Yakov Pechersky]

I would just combine list.range with list.map

[Yakov Pechersky]

There's also docs#list.range' for offset starts

[Diana Kalinichenko]

Yeah, this suffices:

def range_step (l r s : ℕ) : list ℕ :=
  list.map (λ x, s * x + l) $ list.range ((r + s - l - 1) / s)

[Yakov Pechersky]

With all the caveats of nat division and subtraction, of course

[Kevin Buzzard]

I would imagine that this is one of the few cases where the caveats are actually exactly what you want; Python doesn't care if m isn't x mod n.

[Kevin Buzzard]

Note that Python expects integer inputs, not naturals, and then subtraction works fine.