for … in with index

Stream: Is there code for X?

[Joachim Breitner]

What is the idiomatic way to extend a

for x in a do
  …

iteration (where a could be an Array) if I also need the current index? Something like

for i, x in …

or would I iterate only over the indexes and use a.get! i or something else?

[Joachim Breitner]

In the lean code itself I find this idiom:

      for i in List.range params.size do
          let param := params[i]!

[Joachim Breitner]

In other places I see

  let mut i := 0
  for a in as do
    …
    i := i + 1

so I guess the answer is “there is no idiomatic way (yet)”, and whatever works works :-)

[Adam Topaz]

For lists/arrays i think the following looks quite nice:

def foo : Array Nat := #[1,2,3]

#eval show IO Unit from do
  for a in foo, i in [:foo.size] do
    IO.println s!"{i}, {a}"

[Joachim Breitner]

TIL we have parallel iteration.

[Eric Wieser]

For lists, we have docs#List.enum

[Eric Wieser]

But no docs#Array.enum, and presumably that would be inefficient anyway