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

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

Equations

• Vector.finRange n = Vector.ofFn fun (i : Fin n) => i

@[simp]

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

@[simp]

theorem Vector.finRange_zero : Vector.finRange 0 = { toArray := #[], size_toArray := ⋯ }

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

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

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