Theorems about List.ofFn

def List.ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) : List α

ofFn f with f : fin n → α returns the list whose ith element is f i

ofFn f = [f 0, f 1, ... , f (n - 1)]

Equations

• List.ofFn f = Fin.foldr n (fun (x1 : Fin n) (x2 : List α) => f x1 :: x2) []

@[simp]

theorem List.length_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (List.ofFn f).length = n

@[simp]

theorem List.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩

@[simp]

theorem List.getElem?_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) : (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

@[simp]

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

ofFn on an empty domain is the empty list.

@[simp]

theorem List.ofFn_succ {α : Type u_1} {n : Nat} (f : Fin (n + 1) → α) : List.ofFn f = f 0 :: List.ofFn fun (i : Fin n) => f i.succ

@[simp]

theorem List.ofFn_eq_nil_iff {n : Nat} {α : Type u_1} {f : Fin n → α} : List.ofFn f = [] ↔ n = 0

theorem List.head_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).head h = f ⟨0, ⋯⟩

theorem List.getLast_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).getLast h = f ⟨n - 1, ⋯⟩