Theorems about Array.ofFn

@[simp]

theorem Array.ofFn_zero {α : Type u_1} (f : Fin 0 → α) : ofFn f = #[]

theorem Array.ofFn_succ {n : Nat} {α : Type u_1} (f : Fin (n + 1) → α) : ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f ⟨n, ⋯⟩)

@[simp]

theorem Array.toList_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (ofFn f).toList = List.ofFn f

@[simp]

theorem Array.ofFn_eq_empty_iff {n : Nat} {α : Type u_1} {f : Fin n → α} : ofFn f = #[] ↔ n = 0

@[simp]

theorem Array.mem_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a