# 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

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

Instances For

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

- List.ofFnM f = List.reverse <$> Fin.foldlM n (fun (xs : List α) (i : Fin n) => (fun (x : α) => x :: xs) <$> f i) []

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
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)]
source
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)
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, ⋯⟩
source
@[simp]
theorem List.ofFnM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin 0 → m α} :
ofFnM f = pure []

`ofFnM` on an empty domain is the empty list.

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

source
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 as ← ofFnM fun (i : Fin n) => f i.castSucc let a ← f (Fin.last n) pure (as ++ [a])
source
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 as ← ofFnM fun (i : Fin n) => f (Fin.castLE ⋯ i) let bs ← ofFnM fun (i : Fin k) => f (Fin.natAdd n i) pure (as ++ bs)
source
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
source
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
source
@[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 → α} :
ofFnM (pure ∘ f) = pure (ofFn f)
source
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)
source
@[simp]
theorem List.idRun_ofFnM {n : Nat} {α : Type u_1} {f : Fin n → Id α} :
(ofFnM f).run = ofFn fun (i : Fin n) => (f i).run