Documentation

Init.Data.List.OfFn

Theorems about List.ofFn #

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
    def List.ofFnM {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : Fin nm α) :
    m (List α)

    Creates a list wrapped in a monad by applying the monadic function f : Fin n → m α to each potential index in order, starting at 0.

    Equations
    Instances For
      @[simp]
      theorem List.length_ofFn {n : Nat} {α : Type u_1} {f : Fin nα} :
      (ofFn f).length = n
      @[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,
      @[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
      @[simp]
      theorem List.ofFn_zero {α : Type u_1} {f : Fin 0α} :

      ofFn on an empty domain is the empty list.

      @[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
      theorem List.ofFn_succ_last {α : Type u_1} {n : Nat} {f : Fin (n + 1)α} :
      ofFn f = (ofFn fun (i : Fin n) => f i.castSucc) ++ [f (Fin.last n)]
      theorem List.ofFn_add {α : Type u_1} {n m : Nat} {f : Fin (n + m)α} :
      ofFn f = (ofFn fun (i : Fin n) => f (Fin.castLE i)) ++ ofFn fun (i : Fin m) => f (Fin.natAdd n i)
      @[simp]
      theorem List.ofFn_eq_nil_iff {n : Nat} {α : Type u_1} {f : Fin nα} :
      ofFn f = [] n = 0
      @[simp]
      theorem List.mem_ofFn {α : Type u_1} {n : Nat} {f : Fin nα} {a : α} :
      a ofFn f (i : Fin n), f i = a
      theorem List.head_ofFn {α : Type u_1} {n : Nat} {f : Fin nα} (h : ofFn f []) :
      (ofFn f).head h = f 0,
      theorem List.getLast_ofFn {α : Type u_1} {n : Nat} {f : Fin nα} (h : ofFn f []) :
      (ofFn f).getLast h = f n - 1,
      @[simp]
      theorem List.ofFnM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin 0m α} :

      ofFnM on an empty domain is the empty list.

      See Init.Data.List.FinRange for the ofFnM_succ variant.

      theorem List.ofFnM_succ_last {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : Fin (n + 1)m α} :
      ofFnM f = do let asofFnM fun (i : Fin n) => f i.castSucc let af (Fin.last n) pure (as ++ [a])
      theorem List.ofFnM_add {k : Nat} {α : Type u_1} {n : Nat} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {f : Fin (n + k)m α} :
      ofFnM f = do let asofFnM fun (i : Fin n) => f (Fin.castLE i) let bsofFnM fun (i : Fin k) => f (Fin.natAdd n i) pure (as ++ bs)
      theorem Fin.foldl_cons_eq_append {n : Nat} {α : Type u_1} {f : Fin nα} {xs : List α} :
      foldl n (fun (xs : List α) (i : Fin n) => f i :: xs) xs = (List.ofFn f).reverse ++ xs
      theorem Fin.foldr_cons_eq_append {n : Nat} {α : Type u_1} {f : Fin nα} {xs : List α} :
      foldr n (fun (i : Fin n) (xs : List α) => f i :: xs) xs = List.ofFn f ++ xs
      @[simp]
      theorem List.ofFnM_pure_comp {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : Nat} {f : Fin nα} :
      theorem List.ofFnM_pure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : Nat} {f : Fin nα} :
      (ofFnM fun (i : Fin n) => pure (f i)) = pure (ofFn f)
      @[simp]
      theorem List.idRun_ofFnM {n : Nat} {α : Type u_1} {f : Fin nId α} :
      (ofFnM f).run = ofFn fun (i : Fin n) => (f i).run