Documentation

Mathlib.Init.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
Instances For
    def when {m : TypeType} [Monad m] (c : Prop) [Decidable c] (t : m Unit) :
    Equations
    Instances For
      def condM {m : TypeType} [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
      Instances For
        def whenM {m : TypeType} [Monad m] (c : m Bool) (t : m Unit) :
        Equations
        Instances For
          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
          Instances For
            def Monad.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm β) :
            List αm (List β)
            Equations
            Instances For
              def Monad.join {m : Type u_1 → Type u_1} [Monad m] {α : Type u_1} (a : m (m α)) :
              m α
              Equations
              Instances For
                def Monad.filter {m : TypeType u_1} [Monad m] {α : Type} (f : αm Bool) (as : List α) :
                m (List α)
                Equations
                Instances For
                  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
                  Instances For
                    def Monad.cond {m : TypeType} [Monad m] {α : Type} (mbool : m Bool) (tm : m α) (fm : m α) :
                    m α
                    Equations
                    Instances For
                      def Monad.sequence {m : Type u → Type v} [Monad m] {α : Type u} :
                      List (m α)m (List α)
                      Equations
                      Instances For
                        def Monad.sequence' {m : TypeType u} [Monad m] {α : Type} :
                        List (m α)m Unit
                        Equations
                        Instances For
                          def Monad.whenb {m : TypeType} [Monad m] (b : Bool) (t : m Unit) :
                          Equations
                          Instances For
                            def Monad.unlessb {m : TypeType} [Monad m] (b : Bool) (t : m Unit) :
                            Equations
                            Instances For