@[simp]
theorem
Option.foldlM_toList
{m : Type u_1 → Type u_2}
{β : Type u_3}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(o : Option β)
(a : α)
(f : α → β → m α)
:
@[simp]
theorem
Option.foldrM_toList
{m : Type u_1 → Type u_2}
{β : Type u_3}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(o : Option β)
(a : α)
(f : β → α → m α)
:
@[simp]
@[simp]