List.enumerate

Stream: lean4

[Arthur Paulino]

Do these look like functions that would go somewhere in Lean 4? I've needed these a few times...
Maybe somewhere in Init/Data/List/Basic?

def List.enumerateAux : Nat → List α → List (Nat × α)
  | _, nil      => nil
  | n, cons h t => (n, h) :: enumerateAux (n + 1) t

def List.enumerate (l : List α) : List (Nat × α) :=
  l.enumerateAux 0

[Henrik Böving]

Would be even cooler if it was a Fin with upper limit l.length so you could use it in stuff like proofs

[Mario Carneiro]

I would guess it's already in mathlib4, since that exists in lean 3

[Mario Carneiro]

not the dependent version though

[Arthur Paulino]

I know it's hard to draw the line, but I think that adding mathlib as a dependency just to use common programming functions like these is a bit overkill

[Mario Carneiro]

mathlib4 is a lot smaller than mathlib, you know

[Arthur Paulino]

But it's going to grow a lot, right?