Documentation

Mathlib.Control.Basic

Extends the theory on functors, applicatives and monads.

def zipWithM {F : Type u → Type v} [Applicative F] {α₁ : Type u} {α₂ : Type u} {φ : 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} {β : Type u} {γ : 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 α) :
      (Seq.seq (pure fun (x : α) => x) fun (x_1 : Unit) => x) = x
      theorem seq_map_assoc {α : Type u} {β : Type u} {γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F (αβ)) (f : γα) (y : F γ) :
      (Seq.seq x fun (x : Unit) => f <$> y) = Seq.seq ((fun (x : αβ) => x f) <$> x) fun (x : Unit) => y
      theorem map_seq {α : Type u} {β : Type u} {γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (f : βγ) (x : F (αβ)) (y : F α) :
      (f <$> Seq.seq x fun (x : Unit) => y) = Seq.seq ((fun (x : αβ) => f x) <$> x) fun (x : Unit) => y
      theorem seq_bind_eq {α : Type u} {β : Type u} {γ : 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} {β : Type u} (f : αm β) :
      pure >=> f = f
      theorem fish_assoc {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} {β : Type u} {γ : Type u} {φ : Type u} (f : αm β) (g : βm γ) (h : γm φ) :
      (f >=> g) >=> h = f >=> g >=> h
      def List.mapAccumRM {α : Type u} {β' : Type v} {γ' : 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} {γ' : 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} {β : 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 α))) :
          joinM (joinM <$> a) = joinM (joinM a)
          @[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]
                theorem guard_false {F : TypeType v} [Alternative F] {h : Decidable False} :
                guard False = failure
                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
                  • Sum.instMonad_mathlib = Monad.mk
                  Equations
                  • =
                  Equations
                  • =
                  class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulApplicative :

                  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_prod {m : Type u → Type v} :
                    ∀ {inst : Applicative m} [self : CommApplicative m] {α β : Type u} (a : m α) (b : m β), (Seq.seq (Prod.mk <$> a) fun (x : Unit) => b) = Seq.seq ((fun (b : β) (a : α) => (a, b)) <$> b) fun (x : Unit) => a

                    Computations performed first on a : α and then on b : β are equal to those performed in the reverse order.

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