no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM' f l = mapM f l
simp [go, mapM]
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
acc : List β
⊢ mapM.loop f [] acc = do
    let __do_lift ← mapM' f []
    pure (reverse acc ++ __do_lift)
simp
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l✝ : List α
a : α
l : List α
acc : List β
⊢ mapM.loop f (a :: l) acc = do
    let __do_lift ← mapM' f (a :: l)
    pure (reverse acc ++ __do_lift)
simp [go l]