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 < n → m β)
(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.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 β)
:
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 β)
:
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 < n → m β)
: