enumerate Array items: (0, item[0]), (1, item[1]) etc.

Stream: Is there code for X?

[Michael Rothgang]

Is there a way to enumerate the items of a list or an array nicely, similar to Python's enumerate?
Enabling something like

import Mathlib
def foo (input : List Int) := do
  for (i, x) in enumerate input do
    -- real code here
    let _n := 42

[Michael Rothgang]

I do know work-arounds; this is merely a matter of convenience. Things coming to my mind

• iterating over the indices of the array
• can I zip with the natural numbers, as a list? Not sure if iterators are lazy in Lean...

[Michael Rothgang]

to un-#XY: I want to iterate over all lines in a file and have the line number at hand.
Sure, I can write these are a for loop and manually increment a counter, no problem.
But sometimes, writing more functional code would feel nicer.

[Yaël Dillies]

Are you looking for docs#List.enum ?

[Yaël Dillies]

import Mathlib
def foo (input : List Int) := do
  for (i, x) in input.enum do
    -- real code here
    let _n := 42

[Michael Rothgang]

Oh yes, that's what I want! (I wouldn't mind Array.enum either, but I'm in fact not sure if there's a big difference.)