Monad combinators, as in Haskell's Control.Monad.

def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α

Equations

• joinM a = a >>= id

def when {m : Type → Type} [Monad m] (c : Prop) [Decidable c] (t : m Unit) : m Unit

Equations

• when c t = if c then t else pure ()

def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm : m α) (fm : m α) : m α

Equations

• condM mbool tm fm = do let b ← mbool bif b then tm else fm

def whenM {m : Type → Type} [Monad m] (c : m Bool) (t : m Unit) : m Unit

Equations

• whenM c t = condM c t (pure ())

def Monad.mapM {m : Type u_1 → Type u_2} [Monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) (as : List α) : m (List β)

Equations

• @Monad.mapM = @mapM

def Monad.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : List α → m (List β)

Equations

• @Monad.mapM' = @mapM'

def Monad.join {m : Type u_1 → Type u_1} [Monad m] {α : Type u_1} (a : m (m α)) : m α

Equations

• @Monad.join = @joinM

def Monad.filter {m : Type → Type u_1} [Monad m] {α : Type} (f : α → m Bool) (as : List α) : m (List α)

Equations

• @Monad.filter = @filterM

def Monad.foldl {m : Type u_1 → Type u_2} [Monad m] {s : Type u_1} {α : Type u_3} (f : s → α → m s) (init : s) : List α → m s

Equations

• @Monad.foldl = @List.foldlM

def Monad.cond {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm : m α) (fm : m α) : m α

Equations

• @Monad.cond = @condM

def Monad.sequence {m : Type u → Type v} [Monad m] {α : Type u} : List (m α) → m (List α)

Equations

• Monad.sequence [] = pure []
• Monad.sequence (h :: t) = do let h' ← h let t' ← Monad.sequence t pure (h' :: t')

def Monad.sequence' {m : Type → Type u} [Monad m] {α : Type} : List (m α) → m Unit

Equations

• Monad.sequence' [] = pure ()
• Monad.sequence' (h :: t) = SeqRight.seqRight h fun x => Monad.sequence' t

def Monad.whenb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit

Equations

• Monad.whenb b t = bif b then t else pure ()

def Monad.unlessb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit

Equations

• Monad.unlessb b t = bif b then pure () else t