@[inline]

def List.flatMapMTR {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)

Applies a monadic function that returns a list to each element of a list, from left to right, and concatenates the resulting lists.

Equations

• List.flatMapMTR f as = List.flatMapMTR.loop f as []

@[specialize #[]]

def List.flatMapMTR.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) : List α → List (List β) → m (List β)

Equations

• List.flatMapMTR.loop f [] x✝ = pure x✝.reverse.flatten
• List.flatMapMTR.loop f (a :: as) x✝ = do let bs' ← f a List.flatMapMTR.loop f as (bs' :: x✝)

@[csimp]

theorem List.flatMapM_eq_flatMapMTR : @flatMapM = @flatMapMTR