mathlib documentation

control.traversable.instances

Traversable instances #

This file provides instances of traversable for types from the core library: option, list and sum.

source
theorem option.id_traverse {α : Type u_1} (x : option α) :
option.traverse id.mk x = x
source
@[nolint]
theorem option.comp_traverse {F G : Type u → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : option α) :
option.traverse (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (option.traverse f <$> option.traverse g x)
source
theorem option.traverse_eq_map_id {α β : Type u_1} (f : α → β) (x : option α) :
traverse (id.mk ∘ f) x = id.mk (f <$> x)
source
theorem option.naturality {F G : Type u → Type 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 α) :
⇑η (option.traverse f x) = option.traverse (⇑η ∘ f) x
source
@[protected, instance]
def option.is_lawful_traversable  :
is_lawful_traversable option
Equations
source
@[protected]
theorem list.id_traverse {α : Type u_1} (xs : list α) :
list.traverse id.mk xs = xs
source
@[protected, nolint]
theorem list.comp_traverse {F G : Type u → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : list α) :
list.traverse (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (list.traverse f <$> list.traverse g x)
source
@[protected]
theorem list.traverse_eq_map_id {α β : Type u_1} (f : α → β) (x : list α) :
list.traverse (id.mk ∘ f) x = id.mk (f <$> x)
source
@[protected]
theorem list.naturality {F G : Type u → Type 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 α) :
⇑η (list.traverse f x) = list.traverse (⇑η ∘ f) x
source
@[protected, instance]
def list.is_lawful_traversable  :
is_lawful_traversable list
Equations
source
@[simp]
theorem list.traverse_nil {F : Type u → Type u} [applicative F] {α' β' : Type u} (f : α' → F β') :
traverse f list.nil = pure list.nil
source
@[simp]
theorem list.traverse_cons {F : Type u → Type u} [applicative F] {α' β' : Type u} (f : α' → F β') (a : α') (l : list α') :
traverse f (a :: l) = (λ (_x : β') (_y : list β'), _x :: _y) <$> f a <*> traverse f l
source
@[simp]
theorem list.traverse_append {F : Type u → Type 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
source
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
source
@[protected]
theorem sum.traverse_map {σ : Type u} {G : Type u → Type u} [applicative G] {α β γ : Type u} (g : α → β) (f : β → G γ) (x : σ ⊕ α) :
sum.traverse f (g <$> x) = sum.traverse (f ∘ g) x
source
@[protected]
theorem sum.id_traverse {σ α : Type u_1} (x : σ ⊕ α) :
sum.traverse id.mk x = x
source
@[protected, nolint]
theorem sum.comp_traverse {σ : Type u} {F G : Type u → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (f : β → F γ) (g : α → G β) (x : σ ⊕ α) :
sum.traverse (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (sum.traverse f <$> sum.traverse g x)
source
@[protected]
theorem sum.traverse_eq_map_id {σ α β : Type u} (f : α → β) (x : σ ⊕ α) :
sum.traverse (id.mk ∘ f) x = id.mk (f <$> x)
source
@[protected]
theorem sum.map_traverse {σ : Type u} {G : Type u → Type u} [applicative G] [is_lawful_applicative G] {α : Type u_1} {β γ : Type u} (g : α → G β) (f : β → γ) (x : σ ⊕ α) :
functor.map f <$> sum.traverse g x = sum.traverse (functor.map f ∘ g) x
source
@[protected]
theorem sum.naturality {σ : Type u} {F G : Type u → Type 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 : σ ⊕ α) :
⇑η (sum.traverse f x) = sum.traverse (⇑η ∘ f) x
source
@[protected, instance]
def sum.is_lawful_traversable {σ : Type u} :
is_lawful_traversable (sum σ)
Equations