Documentation

Mathlib.Control.Basic

Extends the theory on functors, applicatives and monads.

def zipWithM {F : Type u → Type v} [Applicative F] {α₁ α₂ φ : Type u} (f : α₁α₂F φ) :
List α₁List α₂F (List φ)

A generalization of List.zipWith which combines list elements with an Applicative.

Equations
    Instances For
      def zipWithM' {α β γ : Type u} {F : Type u → Type v} [Applicative F] (f : αβF γ) :
      List αList βF PUnit

      Like zipWithM but evaluates the result as it traverses the lists using *>.

      Equations
        Instances For
          @[simp]
          theorem pure_id'_seq {α : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F α) :
          (pure fun (x : α) => x) <*> x = x
          theorem seq_map_assoc {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F (αβ)) (f : γα) (y : F γ) :
          x <*> f <$> y = (fun (x : αβ) => x f) <$> x <*> y
          theorem map_seq {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (f : βγ) (x : F (αβ)) (y : F α) :
          f <$> (x <*> y) = (fun (x : αβ) => f x) <$> x <*> y
          theorem seq_bind_eq {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m α) {g : βm γ} {f : αβ} :
          f <$> x >>= g = x >>= g f
          theorem fish_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} {β : Type u} (f : αm β) :
          f >=> pure = f
          theorem fish_pipe {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (f : αm β) :
          pure >=> f = f
          theorem fish_assoc {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} {β γ φ : Type u} (f : αm β) (g : βm γ) (h : γm φ) :
          (f >=> g) >=> h = f >=> g >=> h
          def List.mapAccumRM {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : αβ'm' (β' × γ')) :
          β'List αm' (β' × List γ')

          Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the right (i.e., starting from the tail of the list).

          Equations
            Instances For
              def List.mapAccumLM {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : β'αm' (β' × γ')) :
              β'List αm' (β' × List γ')

              Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the left (i.e., starting from the head of the list).

              Equations
                Instances For
                  theorem joinM_map_map {m : Type u → Type u} [Monad m] [LawfulMonad m] {α β : Type u} (f : αβ) (a : m (m α)) :
                  theorem joinM_map_joinM {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m (m (m α))) :
                  @[simp]
                  theorem joinM_map_pure {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m α) :
                  joinM (pure <$> a) = a
                  @[simp]
                  theorem joinM_pure {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m α) :
                  joinM (pure a) = a
                  def succeeds {F : TypeType v} [Alternative F] {α : Type} (x : F α) :

                  Returns pure true if the computation succeeds and pure false otherwise.

                  Equations
                    Instances For
                      def tryM {F : TypeType v} [Alternative F] {α : Type} (x : F α) :

                      Attempts to perform the computation, but fails silently if it doesn't succeed.

                      Equations
                        Instances For
                          def try? {F : TypeType v} [Alternative F] {α : Type} (x : F α) :
                          F (Option α)

                          Attempts to perform the computation, and returns none if it doesn't succeed.

                          Equations
                            Instances For
                              @[simp]
                              theorem guard_true {F : TypeType v} [Alternative F] {h : Decidable True} :
                              @[simp]
                              def Sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} :
                              e α(αe β)e β

                              The monadic bind operation for Sum.

                              Equations
                                Instances For
                                  instance Sum.instMonad_mathlib {e : Type v} :
                                  Equations
                                    class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulApplicative m :

                                    A CommApplicative functor m is a (lawful) applicative functor which behaves identically on α × β and β × α, so computations can occur in either order.

                                    Instances
                                      theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ : Type u} (a : m α) (b : m β) {f : αβγ} :
                                      f <$> a <*> b = flip f <$> b <*> a