mathlib3
chore(data/list/basic): rename take_all -> take_length
#2343
Merged

Commits
  • chore(data/list/basic): rename take_all -> take_length
    Scott Morrison committed 5 years ago
  • also rename drop_all
    Scott Morrison committed 5 years ago
  • Merge branch 'master' into rename_take_all
    mergify[bot] committed 5 years ago
  • Merge branch 'master' into rename_take_all
    mergify[bot] committed 5 years ago
Loading