List.range, but with `Fin n` as elements

Stream: Is there code for X?

[Alex Keizer]

Is there a function that, given an argument n : Nat gives the list [0, 1, ..., n-1], but where the elements are Fin n rather than Nats?

That is, does the following already have a name?

def _root_.List.rangeFin (n : Nat) : List (Fin n) :=
  (List.range n).attach.map fun ⟨i, h⟩ => ⟨i, List.mem_range.mp h⟩

[Eric Wieser]

docs#List.finRange