Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-06 10:29 e93fa306

View on Github →

feat(category/fold): foldl and foldr for traversable structures (#376)

Estimated changes

Created src/category/fold.lean

added def monoid.foldl.mk

added def monoid.foldl.of_free_monoid

added def monoid.foldl

added def monoid.foldr.get

added def monoid.foldr.mk

added def monoid.foldr.of_free_monoid

added def monoid.foldr

added def monoid.mfoldl.mk

added def monoid.mfoldl.of_free_monoid

added def monoid.mfoldl

added def monoid.mfoldr.get

added def monoid.mfoldr.mk

added def monoid.mfoldr.of_free_monoid

added def monoid.mfoldr

added def traversable.fold_map

added theorem traversable.fold_map_hom

added theorem traversable.fold_map_hom_free

added theorem traversable.fold_map_map

added theorem traversable.fold_mfoldl_cons

added theorem traversable.fold_mfoldr_cons

added theorem traversable.foldl.of_free_monoid_comp_free_mk

added def traversable.foldl

added theorem traversable.foldl_map

added theorem traversable.foldl_to_list

added theorem traversable.foldr.of_free_monoid_comp_free_mk

added theorem traversable.foldr.unop_of_free_monoid

added def traversable.foldr

added theorem traversable.foldr_map

added theorem traversable.foldr_to_list

added def traversable.free.map

added theorem traversable.free.map_eq_map

added def traversable.free.mk

added def traversable.length

added theorem traversable.length_to_list

added def traversable.map_fold

added theorem traversable.mfoldl.of_free_monoid_comp_free_mk

added def traversable.mfoldl

added theorem traversable.mfoldl_map

added theorem traversable.mfoldl_to_list

added theorem traversable.mfoldr.of_free_monoid_comp_free_mk

added theorem traversable.mfoldr.unop_of_free_monoid

added def traversable.mfoldr

added theorem traversable.mfoldr_map

added theorem traversable.mfoldr_to_list

added def traversable.to_list

added theorem traversable.to_list_eq_self

added theorem traversable.to_list_map

added theorem traversable.to_list_spec