mathlib documentation

control.traversable.lemmas

Traversing collections #

This file proves basic properties of traversable and applicative functors and defines pure_transformation F, the natural applicative transformation from the identity functor to F.

References #

Inspired by The Essence of the Iterator Pattern.

The natural applicative transformation from the identity functor to F, defined by pure : Π {α}, α → F α.

Equations
theorem traversable.map_traverse {t : Type u Type u} [traversable t] [is_lawful_traversable t] {F : Type u Type u} [applicative F] [is_lawful_applicative F] {α β γ : Type u} (g : α F β) (f : β γ) (x : t α) :
theorem traversable.traverse_map {t : Type u Type u} [traversable t] [is_lawful_traversable t] {F : Type u Type u} [applicative F] [is_lawful_applicative F] {α β γ : Type u} (f : β F γ) (g : α β) (x : t α) :
theorem traversable.id_sequence {t : Type u Type u} [traversable t] [is_lawful_traversable t] {α : Type u} (x : t α) :