def Vector.finRange (n : Nat) : Vector (Fin n) n

finRange n is the vector of all elements of Fin n in order.

@[simp]

theorem Vector.getElem_finRange {n i : Nat} (h : i < n) : (Vector.finRange n)[i] = ⟨i, h⟩

@[simp]

theorem Vector.finRange_zero : Vector.finRange 0 = #v[]

theorem Vector.finRange_succ {n : Nat} : Vector.finRange (n + 1) = Vector.cast ⋯ (#v[0] ++ map Fin.succ (Vector.finRange n))

theorem Vector.finRange_succ_last {n : Nat} : Vector.finRange (n + 1) = map Fin.castSucc (Vector.finRange n) ++ #v[Fin.last n]

theorem Vector.finRange_reverse {n : Nat} : (Vector.finRange n).reverse = map Fin.rev (Vector.finRange n)