Documentation

Mathlib.Control.Combinators

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) :

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) :

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} (p : α → 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 : Unit) => Monad.sequence' t

def Monad.whenb {m : Type → Type} [Monad m] (b : Bool) (t : 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) :

Equations

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