Theorems · Theorem

Traversable.foldrm_toList

∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] (f : α → β → m β) (x : β) (xs : t α),
  Traversable.foldrm f x xs = List.foldrM f x (Traversable.toList xs)

Defined in

Mathlib.Control.Fold

Cited by

0 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Quot.sound

Assumes

TraversableLawfulTraversableMonadLawfulMonad