mathlib3
chore(*): minimise imports of data.list.basic
#2042
Merged

chore(*): minimise imports of data.list.basic #2042

mergify merged 2 commits into master from minimise-imports
kim-em
kim-em chore(*): minimise imports of data.list.basic
db802061
robertylewis
robertylewis approved these changes on 2020-02-23
robertylewis robertylewis added ready-to-merge
mergify[bot] Merge branch 'master' into minimise-imports
9b50d1de
mergify mergify merged 16c1d9d3 into master 6 years ago
mergify mergify deleted the minimise-imports branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone