Results about monadic operations on List, in terms of SatisfiesM. #
theorem
List.satisfiesM_foldlM
{m : Type u_1 → Type u_2}
{β : Type u_1}
{α : Type u_3}
{motive : β → Prop}
{l : List α}
{b : β}
[Monad m]
[LawfulMonad m]
{f : β → α → m β}
(h₀ : motive b)
(h₁ : ∀ (b : β), motive b → ∀ (a : α), a ∈ l → SatisfiesM motive (f b a))
:
SatisfiesM motive (List.foldlM f b l)
theorem
List.satisfiesM_foldrM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{motive : β → Prop}
{l : List α}
{b : β}
[Monad m]
[LawfulMonad m]
{f : α → β → m β}
(h₀ : motive b)
(h₁ : ∀ (a : α), a ∈ l → ∀ (b : β), motive b → SatisfiesM motive (f a b))
:
SatisfiesM motive (List.foldrM f b l)