@[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.

@[specialize #[]]

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

@[csimp]

theorem List.flatMapM_eq_flatMapMTR : @flatMapM = @flatMapMTR