foldrM_eq_foldr — Mathlib

English

For a monad m with LawfulMonad, the monadic right fold is equal to a right fold with bind: foldrM f b l = foldr (λ a mb. mb >>= f a) (pure b) l.

Русский

Для монадического отображения с законной монадой согласованная свёртка справа равна обычной свёртке справа с операцией связывания: foldrM f b l = foldr (λ a mb. mb >>= f a) (pure b) l.

LaTeX

$$$$\operatorname{foldrM} f\, b\, l = \operatorname{foldr}(\lambda a\, mb.\; mb \bind\ f\ a)\; (\operatorname{pure} b)\; l.$$$$

Lean4

theorem foldrM_eq_foldr (f : α → β → m β) (b l) : foldrM f b l = foldr (fun a mb => mb >>= f a) (pure b) l := by
  induction l <;> simp [*]

Похожие утверждения