# Documentation

Mathlib.Control.Traversable.Instances

# IsLawfulTraversable instances #

This file provides instances of IsLawfulTraversable for types from the core library: Option, List and Sum.

theorem Option.id_traverse {α : Type u_1} (x : ) :
theorem Option.comp_traverse {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] {α : Type u_1} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : ) :
Option.traverse (Functor.Comp.mk (fun x x_1 => x <$> x_1) f g) x = theorem Option.traverse_eq_map_id {α : Type u_1} {β : Type u_1} (f : αβ) (x : ) : Option.traverse (pure f) x = pure (f <$> x)
theorem Option.naturality {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] (η : ) {α : Type u_1} {β : Type u} (f : αF β) (x : ) :
(fun {α} => ) () () = Option.traverse ((fun {α} => ) β f) x
Equations
• One or more equations did not get rendered due to their size.
theorem List.id_traverse {α : Type u_1} (xs : List α) :
List.traverse pure xs = xs
theorem List.comp_traverse {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] {α : Type u_1} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : List α) :
List.traverse (Functor.Comp.mk (fun x x_1 => x <$> x_1) f g) x = theorem List.traverse_eq_map_id {α : Type u_1} {β : Type u_1} (f : αβ) (x : List α) : List.traverse (pure f) x = pure (f <$> x)
theorem List.naturality {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] (η : ) {α : Type u_1} {β : Type u} (f : αF β) (x : List α) :
(fun {α} => ) (List β) () = List.traverse ((fun {α} => ) β f) x
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem List.traverse_nil {F : Type u → Type u} [inst : ] {α' : Type u} {β' : Type u} (f : α'F β') :
traverse f [] = pure []
@[simp]
theorem List.traverse_cons {F : Type u → Type u} [inst : ] {α' : Type u} {β' : Type u} (f : α'F β') (a : α') (l : List α') :
traverse f (a :: l) = Seq.seq ((fun x x_1 => x :: x_1) <$> f a) fun x => traverse f l @[simp] theorem List.traverse_append {F : Type u → Type u} [inst : ] {α' : Type u} {β' : Type u} (f : α'F β') [inst : ] (as : List α') (bs : List α') : traverse f (as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f as) fun x => traverse f bs
theorem List.mem_traverse {α' : Type u} {β' : Type u} {f : α'Set β'} (l : List α') (n : List β') :
n traverse f l List.Forall₂ (fun b a => b f a) n l
theorem Sum.traverse_map {σ : Type u} {G : Type u → Type u} [inst : ] {α : Type u} {β : Type u} {γ : Type u} (g : αβ) (f : βG γ) (x : σ α) :
theorem Sum.id_traverse {σ : Type u_1} {α : Type u_1} (x : σ α) :
Sum.traverse pure x = x
theorem Sum.comp_traverse {σ : Type u} {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : σ α) :
Sum.traverse (Functor.Comp.mk (fun x x_1 => x <$> x_1) f g) x = theorem Sum.traverse_eq_map_id {σ : Type u} {α : Type u} {β : Type u} (f : αβ) (x : σ α) : Sum.traverse (pure f) x = pure (f <$> x)
theorem Sum.map_traverse {σ : Type u} {G : Type u → Type u} [inst : ] [inst : ] {α : Type u_1} {β : Type u} {γ : Type u} (g : αG β) (f : βγ) (x : σ α) :
(fun x x_1 => x <$> x_1) f <$> = Sum.traverse ((fun x x_1 => x <\$> x_1) f g) x
theorem Sum.naturality {σ : Type u} {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] (η : ) {α : Type u_1} {β : Type u} (f : αF β) (x : σ α) :
(fun {α} => ) (σ β) () = Sum.traverse ((fun {α} => ) β f) x
Equations
• One or more equations did not get rendered due to their size.