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

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

mergify merged 4 commits into master from rename_take_all
kim-em
chore(data/list/basic): rename take_all -> take_length
b5743726
also rename drop_all
8602959b
cipher1024
cipher1024 approved these changes on 2020-04-07
cipher1024 cipher1024 added ready-to-merge
mergify[bot] Merge branch 'master' into rename_take_all
4ee10d40
mergify[bot] Merge branch 'master' into rename_take_all
b271f1a6
mergify mergify merged 2f2e016e into master 5 years ago
mergify mergify deleted the rename_take_all branch 5 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone