mathlib
77e76ee5 - feat(data/list/basic): add last'_append and head'_append_of_ne_nil (#12221)

Commit
3 years ago
feat(data/list/basic): add last'_append and head'_append_of_ne_nil (#12221) we already have `head'_append` and `last'_append_of_ne_nil`, and users might expect a symmetric API.
Author
Parents
Loading