Documentation

Batteries.Data.Vector.Monadic

theorem Vector.toArray_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] (a : Vector α n) (f : (i : Nat) → αi < nm β) :
toArray <$> a.mapFinIdxM f = a.mapFinIdxM fun (i : Nat) (x : α) (h : i < a.size) => f i x
theorem Vector.toArray_mapFinIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] (a : Vector α n) (f : (i : Nat) → αi < nm β) (i j : Nat) (inv : i + j = n) (bs : Vector β (n - i)) :
toArray <$> mapFinIdxM.map a f i j inv bs = Array.mapFinIdxM.map a.toArray (fun (i : Nat) (x : α) (h : i < a.size) => f i x ) i j bs.toArray
theorem Vector.toArray_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] (a : Vector α n) (f : Natαm β) :
theorem Vector.mapM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : αm β) :
mapM f { toArray := a, size_toArray := h } = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | a_1, h' => { toArray := a_1, size_toArray := }) <$> satisfying
theorem Vector.mapIdxM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : Natαm β) :
mapIdxM f { toArray := a, size_toArray := h } = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | a_1, h' => { toArray := a_1, size_toArray := }) <$> satisfying
theorem Vector.mapFinIdxM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : (i : Nat) → αi < nm β) :
{ toArray := a, size_toArray := h }.mapFinIdxM f = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | a_1, h' => { toArray := a_1, size_toArray := }) <$> satisfying