source
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

Instances For

source
@[simp]
theorem Vector.getElem_finRange {n i : Nat} (h : i < n) :
(Vector.finRange n)[i] = ⟨i, h⟩
source
@[simp]
theorem Vector.finRange_zero :
Vector.finRange 0 = #v[]
source
theorem Vector.finRange_succ {n : Nat} :
Vector.finRange (n + 1) = Vector.cast ⋯ (#v[0] ++ map Fin.succ (Vector.finRange n))
source
theorem Vector.finRange_succ_last {n : Nat} :
Vector.finRange (n + 1) = map Fin.castSucc (Vector.finRange n) ++ #v[Fin.last n]
source
theorem Vector.finRange_reverse {n : Nat} :
(Vector.finRange n).reverse = map Fin.rev (Vector.finRange n)