mathlib documentation

control.traversable.instances

theorem option.id_traverse {α : Type u_1} (x : option α) :

@[nolint]
theorem option.comp_traverse {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : option α) :

theorem option.traverse_eq_map_id {α β : Type u_1} (f : α → β) (x : option α) :
traverse (id.mk f) x = id.mk (f <$> x)

theorem option.naturality {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : option α) :

theorem list.id_traverse {α : Type u_1} (xs : list α) :

@[nolint]
theorem list.comp_traverse {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : list α) :

theorem list.traverse_eq_map_id {α β : Type u_1} (f : α → β) (x : list α) :

theorem list.naturality {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : list α) :

@[simp]
theorem list.traverse_nil {F : Type uType u} [applicative F] {α' β' : Type u} (f : α' → F β') :

@[simp]
theorem list.traverse_cons {F : Type uType u} [applicative F] {α' β' : Type u} (f : α' → F β') (a : α') (l : list α') :
traverse f (a :: l) = (λ (_x : β') (_y : list β'), _x :: _y) <$> f a <*> traverse f l

@[simp]
theorem list.traverse_append {F : Type uType u} [applicative F] {α' β' : Type u} (f : α' → F β') [is_lawful_applicative F] (as bs : list α') :
traverse f (as ++ bs) = append <$> traverse f as <*> traverse f bs

theorem list.mem_traverse {α' β' : Type u} {f : α' → set β'} (l : list α') (n : list β') :
n traverse f l list.forall₂ (λ (b : β') (a : α'), b f a) n l

theorem sum.traverse_map {σ : Type u} {G : Type uType u} [applicative G] {α β γ : Type u} (g : α → β) (f : β → G γ) (x : «σ» α) :

theorem sum.id_traverse {σ α : Type u_1} (x : «σ» α) :

@[nolint]
theorem sum.comp_traverse {σ : Type u} {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : «σ» α) :

theorem sum.traverse_eq_map_id {σ α β : Type u} (f : α → β) (x : «σ» α) :

theorem sum.map_traverse {σ : Type u} {G : Type uType u} [applicative G] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (g : α → G β) (f : β → γ) (x : «σ» α) :

theorem sum.naturality {σ : Type u} {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u_1} {β : Type u} (f : α → F β) (x : «σ» α) :