mathlib3
fd48ac55 - chore(data/list): extract sublists to a separate file (#7757)

Commit
4 years ago
chore(data/list): extract sublists to a separate file (#7757) Minor splitting in `data/list/basic`, splitting out `sublists` to its own file, thereby delaying importing `data.nat.choose` in the `list` development. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading