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 (mk a h) = (fun (x : { a_1 : Array β // a_1.size = a.size }) =>
match x with
| ⟨a_1, h'⟩ => mk a_1 ⋯) <$> 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 (mk a h) = (fun (x : { a_1 : Array β // a_1.size = a.size }) =>
match x with
| ⟨a_1, h'⟩ => mk a_1 ⋯) <$> 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 < n → m β)
:
(mk a h).mapFinIdxM f = (fun (x : { a_1 : Array β // a_1.size = a.size }) =>
match x with
| ⟨a_1, h'⟩ => mk a_1 ⋯) <$> satisfying ⋯