Commit 2023-04-10 18:30 0248d138

View on Github →

feat: port Control.Fold (#2341)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Fold.lean

added def Monoid.Foldl.get

added def Monoid.Foldl.mk

added def Monoid.Foldl.ofFreeMonoid

added def Monoid.Foldl

added def Monoid.Foldr.get

added def Monoid.Foldr.mk

added def Monoid.Foldr.ofFreeMonoid

added def Monoid.Foldr

added def Monoid.foldlM.get

added def Monoid.foldlM.mk

added def Monoid.foldlM.ofFreeMonoid

added def Monoid.foldlM

added def Monoid.foldrM.get

added def Monoid.foldrM.mk

added def Monoid.foldrM.ofFreeMonoid

added def Monoid.foldrM

added theorem Traversable.Free.map_eq_map

added def Traversable.foldMap

added theorem Traversable.foldMap_hom

added theorem Traversable.foldMap_hom_free

added theorem Traversable.foldMap_map

added theorem Traversable.foldl.ofFreeMonoid_comp_of

added theorem Traversable.foldl.unop_ofFreeMonoid

added def Traversable.foldl

added theorem Traversable.foldl_map

added theorem Traversable.foldl_toList

added theorem Traversable.foldlm.ofFreeMonoid_comp_of

added def Traversable.foldlm

added theorem Traversable.foldlm_map

added theorem Traversable.foldlm_toList

added theorem Traversable.foldr.ofFreeMonoid_comp_of

added def Traversable.foldr

added theorem Traversable.foldr_map

added theorem Traversable.foldr_toList

added theorem Traversable.foldrm.ofFreeMonoid_comp_of

added def Traversable.foldrm

added theorem Traversable.foldrm_map

added theorem Traversable.foldrm_toList

added def Traversable.length

added theorem Traversable.length_toList

added def Traversable.mapFold

added def Traversable.toList

added theorem Traversable.toList_eq_self

added theorem Traversable.toList_map

added theorem Traversable.toList_spec