mathlib3
chore(data/list/basic): rename take_all -> take_length
#2343
Merged
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
4
Changes
View On
GitHub
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