Zulip Chat Archive

Stream: Is there code for X?

Topic: range with step


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Feb 14 2021 at 15:40):

I would just combine list.range with list.map

view this post on Zulip Yakov Pechersky (Feb 14 2021 at 15:41):

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

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Feb 14 2021 at 16:15):

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

view this post on Zulip 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.

view this post on Zulip 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