-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore(data/fintype): move results depending on big_operators #2044
Conversation
Looks good to me. |
Another source of recompiles: |
Oof, yes, let's break the chain of imports there. I don't think that "basic facts about lists" should require you to know about ordered rings. Not in this PR, however. |
That's not actually an unreasonable import. |
@jcommelin, want to mark as ready to merge? |
…ver-community#2044) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…ver-community#2044) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
This is just rearranging some results. In particular, this PR makes
data.fintype
not depend onalgebra.big_operators
, and thus needs to move a few results to a new filedata.fintype.card
.I've been wanting to do this for a long time, as I perpetually notice that "easy" bits of the library seem to require recompiling the whole algebraic hierarchy when something in basic tactics changes, and I'm pretty sure the dependency is often via
fintype
importingalgebra.big_operators
, which then imports everything else.I appreciate that reducing compile times is not the greatest principle for deciding how files get divided up ... but compile times are still a huge hassle at the moment.