mathlib3 documentation

control.traversable.instances

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.

theorem option.id_traverse {α : Type u_1} (x : option α) :
@[nolint]
theorem option.traverse_eq_map_id {α β : Type u_1} (f : α β) (x : option α) :
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 α) :
@[protected]
theorem list.id_traverse {α : Type u_1} (xs : list α) :
@[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 α) :
@[protected]
theorem list.traverse_eq_map_id {α β : Type u_1} (f : α β) (x : list α) :
@[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 α) :
@[simp]
theorem list.traverse_nil {F : Type u Type u} [applicative F] {α' β' : Type u} (f : α' F β') :
@[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 α') :
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 : σ α) :
@[protected]
theorem sum.id_traverse {σ α : Type u_1} (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 : σ α) :
@[protected]
theorem sum.traverse_eq_map_id {σ α β : Type u} (f : α β) (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 : σ α) :
@[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 : σ α) :