Zulip Chat Archive
Stream: general
Topic: multiset.lean
Kenny Lau (Feb 21 2019 at 18:44):
Is data/multiset.lean too long?
Kevin Buzzard (Feb 21 2019 at 19:08):
Are you learning some of our British irony here Kenny?
Kenny Lau (Feb 21 2019 at 19:12):
no I mean the file is like 2000+ lines long
Chris Hughes (Feb 21 2019 at 19:14):
Long files aren't as much of a problem as too many imports that aren't used by files that import it. I don't think multiset.lean has this problem.
Kevin Buzzard (Feb 21 2019 at 19:15):
I think it's 3000+ lines long. Sure it's too long. But most of it is very useful and it all belongs to the multiset namespace.
Kevin Buzzard (Feb 21 2019 at 19:21):
I guess multiset could become a one line file "import multiset1 multiset2 multiset3" or something
Last updated: Dec 20 2023 at 11:08 UTC