Theorems about Vector.ofFn

@[simp]

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

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

@[simp]

theorem Vector.mem_ofFn {α : Type u_1} {n : Nat} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a

theorem Vector.back_ofFn {α : Type u_1} {n : Nat} [NeZero n] {f : Fin n → α} : (ofFn f).back = f ⟨n - 1, ⋯⟩

theorem Vector.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 Vector.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)

theorem Vector.ofFn_succ' {n : Nat} {α : Type u_1} {f : Fin (n + 1) → α} : ofFn f = Vector.cast ⋯ ({ toArray := #[f 0], size_toArray := ⋯ } ++ ofFn fun (i : Fin n) => f i.succ)

ofFnM

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

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

Equations

• Vector.ofFnM f = Vector.ofFnM.go f 0 ⋯ (Array.emptyWithCapacity n) ⋯

@[irreducible]

def Vector.ofFnM.go {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : Fin n → m α) (i : Nat) (h' : i ≤ n) (acc : Array α) (w : acc.size = i) : m (Vector α n)

Auxiliary for ofFn. ofFn.go f i acc = acc ++ #v[f i, ..., f(n - 1)]

Equations

• Vector.ofFnM.go f i h' acc w = if h : i < n then do let __do_lift ← f ⟨i, h⟩ Vector.ofFnM.go f (i + 1) ⋯ (acc.push __do_lift) ⋯ else pure { toArray := acc, size_toArray := ⋯ }

@[simp]

theorem Vector.ofFnM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] {f : Fin 0 → m α} : ofFnM f = pure { toArray := #[], size_toArray := ⋯ }

theorem Vector.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 as ← ofFnM fun (i : Fin n) => f i.castSucc let a ← f (Fin.last n) pure (as.push a)

theorem Vector.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)

@[simp]

theorem Vector.toArray_ofFnM {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : toArray <$> ofFnM f = Array.ofFnM f

@[simp]

theorem Vector.toList_ofFnM {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : toList <$> ofFnM f = List.ofFnM f

theorem Vector.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 a ← f 0 let as ← ofFnM fun (i : Fin n) => f i.succ pure (Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ as))

@[simp]

theorem Vector.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)

theorem Vector.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 Vector.idRun_ofFnM {n : Nat} {α : Type u_1} {f : Fin n → Id α} : (ofFnM f).run = ofFn fun (i : Fin n) => (f i).run