Stream: Is there code for X?
Topic: range with step
Diana Kalinichenko (Feb 14 2021 at 15:32):
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 (Feb 14 2021 at 15:40):
I would just combine
Yakov Pechersky (Feb 14 2021 at 15:41):
There's also docs#list.range' for offset starts
Diana Kalinichenko (Feb 14 2021 at 16:14):
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 (Feb 14 2021 at 16:15):
With all the caveats of nat division and subtraction, of course
Kevin Buzzard (Feb 14 2021 at 17:52):
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 (Feb 14 2021 at 17:54):
Note that Python expects integer inputs, not naturals, and then subtraction works fine.
Last updated: May 07 2021 at 17:36 UTC