mathlib3 documentation

control.bitraversable.instances

Bitraversable instances #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
Equations
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
@[protected, instance]
Equations
@[nolint]
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
@[protected, instance]
Equations
def flip.bitraverse {t : Type u Type u Type u} [bitraversable t] {F : Type u Type u} [applicative F] {α α' β β' : Type u} (f : α F α') (f' : β F β') :
flip t α β F (flip t α' β')

The bitraverse function for flip.

Equations
def bicompl.bitraverse {t : Type u Type u Type u} [bitraversable t] (F G : Type u Type u) [traversable F] [traversable G] {m : Type u Type u} [applicative m] {α β α' β' : Type u} (f : α m β) (f' : α' m β') :
function.bicompl t F G α α' m (function.bicompl t F G β β')

The bitraverse function for bicompl.

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} (f : α m β) (f' : α' m β') :
function.bicompr F t α α' m (function.bicompr F t β β')

The bitraverse function for bicompr.

Equations