mathlib
16c1d9d3 - chore(*): minimise imports of data.list.basic (#2042)

Commit

6 years ago

chore(*): minimise imports of data.list.basic (#2042) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

Author

kim-em

Parents