Documentation

Init.Data.List.OfFn

Theorems about List.ofFn #

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

Creates a list by applying f to each potential index in order, starting at 0.

Examples:

  • List.ofFn (n := 3) toString = ["0", "1", "2"]
  • List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]
Equations
Instances For
    source
    @[simp]
    theorem List.length_ofFn {n : Nat} {α : Type u_1} {f : Fin n → α} :
    (ofFn f).length = n
    source
    @[simp]
    theorem List.getElem_ofFn {n : Nat} {α : Type u_1} {i : Nat} {f : Fin n → α} (h : i < (ofFn f).length) :
    (ofFn f)[i] = f ⟨i, ⋯⟩
    source
    @[simp]
    theorem List.getElem?_ofFn {n : Nat} {α : Type u_1} {i : Nat} {f : Fin n → α} :
    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
    source
    @[simp]
    theorem List.ofFn_zero {α : Type u_1} {f : Fin 0 → α} :
    ofFn f = []

    ofFn on an empty domain is the empty list.

    source
    @[simp]
    theorem List.ofFn_succ {α : Type u_1} {n : Nat} {f : Fin (n + 1) → α} :
    ofFn f = f 0 :: ofFn fun (i : Fin n) => f i.succ
    source
    @[simp]
    theorem List.ofFn_eq_nil_iff {n : Nat} {α : Type u_1} {f : Fin n → α} :
    ofFn f = [] ↔ n = 0
    source
    @[simp]
    theorem List.mem_ofFn {α : Type u_1} {n : Nat} {f : Fin n → α} {a : α} :
    a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a
    source
    theorem List.head_ofFn {α : Type u_1} {n : Nat} {f : Fin n → α} (h : ofFn f ≠ []) :
    (ofFn f).head h = f ⟨0, ⋯⟩
    source
    theorem List.getLast_ofFn {α : Type u_1} {n : Nat} {f : Fin n → α} (h : ofFn f ≠ []) :
    (ofFn f).getLast h = f ⟨n - 1, ⋯⟩