# Documentation

## Mathlib.Init.Control.Combinators

def joinM {m : Type u → Type u} [] {α : Type u} (a : m (m α)) :
m α
Equations
Instances For
def when {m : } [] (c : Prop) [] (t : m Unit) :
Equations
• when c t = if c then t else
Instances For
def condM {m : } [] {α : Type} (mbool : m Bool) (tm : m α) (fm : m α) :
m α
Equations
• condM mbool tm fm = do let bmbool bif b then tm else fm
Instances For
def whenM {m : } [] (c : m Bool) (t : m Unit) :
Equations
Instances For
def Monad.mapM {m : Type u_1 → Type u_2} [] {α : Type u_3} {β : Type u_1} (f : αm β) (as : List α) :
m (List β)
Equations
Instances For
def Monad.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αm β) :
List αm (List β)
Equations
Instances For
def Monad.join {m : Type u_1 → Type u_1} [] {α : Type u_1} (a : m (m α)) :
m α
Equations
Instances For
def Monad.filter {m : TypeType u_1} [] {α : Type} (p : αm Bool) (as : List α) :
m (List α)
Equations
Instances For
def Monad.foldl {m : Type u_1 → Type u_2} [] {s : Type u_1} {α : Type u_3} (f : sαm s) (init : s) :
List αm s
Equations
Instances For
def Monad.cond {m : } [] {α : Type} (mbool : m Bool) (tm : m α) (fm : m α) :
m α
Equations
Instances For
def Monad.sequence {m : Type u → Type v} [] {α : Type u} :
List (m α)m (List α)
Equations
Instances For
def Monad.sequence' {m : TypeType u} [] {α : Type} :
List (m α)m Unit
Equations
Instances For
def Monad.whenb {m : } [] (b : Bool) (t : m Unit) :
Equations
• = bif b then t else
Instances For
def Monad.unlessb {m : } [] (b : Bool) (t : m Unit) :
Equations
• = bif b then else t
Instances For