Documentation

Mathlib.Control.Bitraversable.Instances

Bitraversable instances #

This file provides Bitraversable instances for concrete bifunctors:

References #

Tags #

traversable bitraversable functor bifunctor applicative

def Prod.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
α × βF (α' × β')

The bitraverse function for α × β.

Equations
Instances For
    def Sum.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
    α βF (α' β')

    The bitraverse function for α ⊕ β.

    Equations
    Instances For
      def Const.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
      Functor.Const α βF (Functor.Const α' β')

      The bitraverse function for Const. It throws away the second map.

      Equations
      Instances For
        def flip.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} [Applicative F] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF α') (f' : βF β') :
        flip t α βF (flip t α' β')

        The bitraverse function for flip.

        Equations
        Instances For
          instance Bitraversable.flip {t : Type u → Type u → Type u} [Bitraversable t] :
          Equations
          Equations
          • =
          @[instance 10]
          instance Bitraversable.traversable {t : Type u → Type u → Type u} [Bitraversable t] {α : Type u} :
          Equations
          @[instance 10]
          Equations
          • =
          def Bicompl.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) (G : Type u → Type u) [Traversable F] [Traversable G] {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} {α' : Type u} {β' : Type u} (f : αm β) (f' : α'm β') :
          Function.bicompl t F G α α'm (Function.bicompl t F G β β')

          The bitraverse function for bicompl.

          Equations
          Instances For
            instance instBitraversableBicompl {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) (G : Type u → Type u) [Traversable F] [Traversable G] :
            Equations
            def Bicompr.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) [Traversable F] {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} {α' : Type u} {β' : Type u} (f : αm β) (f' : α'm β') :
            Function.bicompr F t α α'm (Function.bicompr F t β β')

            The bitraverse function for bicompr.

            Equations
            Instances For