m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun s a => f a s) b (reverse (a :: l)) = List.foldlM (fun s a => f a s) b (reverse l) >>= f a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ foldrM f b (a :: l) = foldrM f b l >>= f a
simp only [foldrM]
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun s a => f a s) b (reverse (a :: l)) = List.foldlM (fun s a => f a s) b (reverse l) >>= f a
induction l <;> simp_all