Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-24 16:33 f9cf9d39

View on Github →

feat(category/traversable): basic classes for traversable collections

Estimated changes

Created category/traversable/basic.lean

added theorem applicative_transformation.preserves_map

added theorem applicative_transformation.preserves_pure

added theorem applicative_transformation.preserves_seq

added structure applicative_transformation

added def sequence

Created category/traversable/default.lean

Created category/traversable/instances.lean

added theorem id.comp_traverse

added theorem id.id_traverse

added theorem id.map_traverse

added theorem id.naturality

added theorem id.traverse_map

added theorem list.comp_traverse

added theorem list.id_traverse

added theorem list.map_traverse

added theorem list.naturality

added theorem list.traverse_map

added theorem option.comp_traverse

added theorem option.id_traverse

added theorem option.map_traverse

added theorem option.naturality

added theorem option.traverse_map

Created category/traversable/lemmas.lean

added theorem traversable.comp_sequence

added theorem traversable.id_sequence

added theorem traversable.naturality'

added def traversable.pure_transformation

added theorem traversable.purity

added theorem traversable.traverse_eq_map_ident