control.bitraversable.instances

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

flip.bitraverse f f' = bitraversable.bitraverse f' f

source

@[protected, instance]

def bitraversable.flip {t : Type u → Type u → Type u} [bitraversable t] :

bitraversable (flip t)

Equations

bitraversable.flip = {to_bifunctor := bifunctor.flip bitraversable.to_bifunctor, bitraverse := flip.bitraverse _inst_1}

source

@[protected, instance]

def is_lawful_bitraversable.flip {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] :

is_lawful_bitraversable (flip t)

Equations

is_lawful_bitraversable.flip = {to_is_lawful_bifunctor := is_lawful_bifunctor.flip is_lawful_bitraversable.to_is_lawful_bifunctor, id_bitraverse := _, comp_bitraverse := _, bitraverse_eq_bimap_id := _, binaturality := _}

source

@[protected, instance]

def bitraversable.traversable {t : Type u → Type u → Type u} [bitraversable t] {α : Type u} :

traversable (t α)

Equations

bitraversable.traversable = {to_functor := bifunctor.functor α, traverse := bitraversable.tsnd α}

source

@[protected, instance]

def bitraversable.is_lawful_traversable {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α : Type u} :

is_lawful_traversable (t α)

Equations

bitraversable.is_lawful_traversable = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}

source

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

bicompl.bitraverse F G f f' = bitraversable.bitraverse (traversable.traverse f) (traversable.traverse f')

source

@[protected, instance]

def function.bicompl.bitraversable {t : Type u → Type u → Type u} [bitraversable t] (F G : Type u → Type u) [traversable F] [traversable G] :

bitraversable (function.bicompl t F G)

Equations

function.bicompl.bitraversable F G = {to_bifunctor := function.bicompl.bifunctor F G traversable.to_functor, bitraverse := bicompl.bitraverse F G _inst_3}

source

@[protected, instance]

def function.bicompl.is_lawful_bitraversable {t : Type u → Type u → Type u} [bitraversable t] (F G : Type u → Type u) [traversable F] [traversable G] [is_lawful_traversable F] [is_lawful_traversable G] [is_lawful_bitraversable t] :

is_lawful_bitraversable (function.bicompl t F G)

Equations

function.bicompl.is_lawful_bitraversable F G = {to_is_lawful_bifunctor := function.bicompl.is_lawful_bifunctor F G is_lawful_bitraversable.to_is_lawful_bifunctor, id_bitraverse := _, comp_bitraverse := _, bitraverse_eq_bimap_id := _, binaturality := _}

source

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