# Results about monadic operations on `List`, in terms of `SatisfiesM`. #

source
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 (foldlM f b l)
source
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 (foldrM f b l)