mathlib
2f2e016e - chore(data/list/basic): rename take_all -> take_length (#2343)

Commit
5 years ago
chore(data/list/basic): rename take_all -> take_length (#2343) * chore(data/list/basic): rename take_all -> take_length * also rename drop_all Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading