Traversable instances #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides instances of traversable for types from the core library: option, list and
sum.
@[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)
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
@[protected, instance]
Equations
- option.is_lawful_traversable = {to_is_lawful_functor := option.is_lawful_traversable._proof_1, id_traverse := option.id_traverse, comp_traverse := option.comp_traverse, traverse_eq_map_id := option.traverse_eq_map_id, naturality := option.naturality}
@[protected]
@[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)
@[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
@[protected, instance]
Equations
- list.is_lawful_traversable = {to_is_lawful_functor := list.is_lawful_traversable._proof_1, id_traverse := list.id_traverse, comp_traverse := list.comp_traverse, traverse_eq_map_id := list.traverse_eq_map_id, naturality := list.naturality}
@[simp]
@[simp]
theorem
list.traverse_cons
{F : Type u → Type u}
[applicative F]
{α' β' : Type u}
(f : α' → F β')
(a : α')
(l : list α') :
traversable.traverse f (a :: l) = (λ (_x : β') (_y : list β'), _x :: _y) <$> f a <*> traversable.traverse f l
@[simp]
theorem
list.traverse_append
{F : Type u → Type u}
[applicative F]
{α' β' : Type u}
(f : α' → F β')
[is_lawful_applicative F]
(as bs : list α') :
traversable.traverse f (as ++ bs) = has_append.append <$> traversable.traverse f as <*> traversable.traverse f bs
theorem
list.mem_traverse
{α' β' : Type u}
{f : α' → set β'}
(l : list α')
(n : list β') :
n ∈ traversable.traverse f l ↔ list.forall₂ (λ (b : β') (a : α'), b ∈ f a) n l
@[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
@[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)
@[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
@[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
@[protected, instance]
Equations
- sum.is_lawful_traversable = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}