Documentation

Init.Data.Array.OfFn

Theorems about Array.ofFn #

ofFn #

@[simp]
theorem Array.ofFn_zero {α : Type u_1} {f : Fin 0α} :
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, )
theorem Array.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.toArray_ofFn {n : Nat} {α : Type u_1} {f : Fin nα} :
@[simp]
theorem Array.toList_ofFn {n : Nat} {α : Type u_1} {f : Fin nα} :
theorem Array.ofFn_succ' {n : Nat} {α : Type u_1} {f : Fin (n + 1)α} :
ofFn f = #[f 0] ++ ofFn fun (i : Fin n) => f i.succ
@[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

ofFnM #

def Array.ofFnM {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : Fin nm α) :
m (Array α)

Construct (in a monadic context) an array by applying a monadic function to each index.

Equations
Instances For
    @[simp]
    theorem Array.ofFnM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] {f : Fin 0m α} :
    theorem Array.ofFnM_succ' {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 af 0 let asofFnM fun (i : Fin n) => f i.succ pure (#[a] ++ as)
    theorem Array.ofFnM_succ {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.push a)
    theorem Array.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)
    @[simp]
    theorem Array.toList_ofFnM {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin nm α} :
    @[simp]
    theorem Array.ofFnM_pure_comp {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : Nat} {f : Fin nα} :
    theorem Array.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 Array.idRun_ofFnM {n : Nat} {α : Type u_1} {f : Fin nId α} :
    (ofFnM f).run = ofFn fun (i : Fin n) => (f i).run