Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-15 20:47 bde21328

View on Github →

feat(category/traversable): derive traversable instances Authors: Simon Hudon, Mario Carneiro

Estimated changes

added theorem applicative.ext
modified theorem applicative.map_seq_map
modified theorem comp.map_pure
modified theorem comp.pure_seq_eq_map
modified theorem comp.seq_assoc
modified theorem comp.seq_pure
added def list.mpartition
modified theorem map_seq
modified def mtry
modified def mzip_with'
modified theorem pure_id'_seq
modified theorem seq_map_assoc
modified def succeeds
modified theorem functor.comp.map_mk
added def functor.comp.mk
added def functor.comp.run
added def functor.comp
deleted structure functor.comp
added theorem functor.ext
modified def sequence
deleted theorem id.comp_traverse
deleted theorem id.id_traverse
deleted theorem id.map_traverse
deleted theorem id.naturality
deleted theorem id.traverse_map
modified theorem list.comp_traverse
modified theorem list.id_traverse
deleted theorem list.map_traverse
modified theorem list.naturality
deleted theorem list.traverse_map
modified theorem option.comp_traverse
modified theorem option.id_traverse
deleted theorem option.map_traverse
modified theorem option.naturality
deleted theorem option.traverse_map
modified theorem traversable.comp_sequence
modified theorem traversable.naturality'
deleted theorem traversable.purity
added def vector.to_array
added inductive either
added structure my_struct2
added structure my_struct
added inductive rec_data3