mathlib
6a6beaa7 - chore(data/list/basic): drop `append_foldl` and `append_foldr`, add `map_nil` and `prod_singleton` (#2057)

Commit
5 years ago
chore(data/list/basic): drop `append_foldl` and `append_foldr`, add `map_nil` and `prod_singleton` (#2057) `append_foldl` and `append_foldr` were unused duplicates of `foldl_append` and `foldr_append` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading