mathlib documentation

control.bitraversable.instances

bitraversable instances

Instances

References

Tags

traversable bitraversable functor bifunctor applicative

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

Equations
@[instance]

Equations
def sum.bitraverse {F : Type uType u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') :
α βF (α' β')

Equations
@[instance]

Equations
def const.bitraverse {F : Type uType u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') :
functor.const α βF (functor.const α' β')

Equations
@[instance]

Equations
def flip.bitraverse {t : Type uType uType u} [bitraversable t] {F : Type uType u} [applicative F] {α α' β β' : Type u} (f : α → F α') (f' : β → F β') :
flip t α βF (flip t α' β')

Equations
@[instance]
def bitraversable.flip {t : Type uType uType u} [bitraversable t] :

Equations
@[instance]
def bitraversable.traversable {t : Type uType uType u} [bitraversable t] {α : Type u} :

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

Equations
@[instance]
def function.bicompl.bitraversable {t : Type uType uType u} [bitraversable t] (F G : Type uType u) [traversable F] [traversable G] :

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

Equations