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

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

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 : Nat} (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)