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

Returns an array of all elements of Fin n in order, starting at 0.

Examples:

• Array.finRange 0 = (#[] : Array (Fin 0))
• Array.finRange 2 = (#[0, 1] : Array (Fin 2))

Equations

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

@[simp]

theorem Array.size_finRange {n : Nat} : (Array.finRange n).size = n

@[simp]

theorem Array.getElem_finRange {n i : Nat} (h : i < (Array.finRange n).size) : (Array.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩

@[simp]

theorem Array.finRange_zero : Array.finRange 0 = #[]

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

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

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