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
move(data/set/pointwise/interval): Sanitise imports #17347
Conversation
Great, thanks, this looks promising. I'll check if there's any value to #17340 after this merges. bors d+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
@@ -3,6 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved. | |||
Released under Apache 2.0 license as described in the file LICENSE. | |||
Authors: Yaël Dillies | |||
-/ | |||
import data.fin.basic |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just noting for later: this import is bogus. I remember adding the few fin
lemmas at the bottom of the file because that was the first place where I had both access to covby
and fin
(due to the bogus import this PR is fixing), but those lemmas have nothing to do with succ
/pred
on nat
.
bors merge |
Quite a lot of pure order theory files import `data.set.intervals.unordered_interval`, which itself imports `data.set.intervals.image_preimage`, which in turn imports a lot of algebra. If we change the order of dependency between `data.set.intervals.unordered_interval` and `data.set.intervals.image_preimage`, we avoid algebra leaking into pure order theory and drastically reduce imports for many files. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed (retrying...): |
Canceled. |
There was a merge conflict with master, unfortunately. bors merge p=25 |
Quite a lot of pure order theory files import `data.set.intervals.unordered_interval`, which itself imports `data.set.intervals.image_preimage`, which in turn imports a lot of algebra. If we change the order of dependency between `data.set.intervals.unordered_interval` and `data.set.intervals.image_preimage`, we avoid algebra leaking into pure order theory and drastically reduce imports for many files. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
This is going to merged as part of #17381. I'm closing now to conserve CI resources. |
This is the supremum of * #17376 * #17375 * #17374 * #17362 * #17355 * #17349 * #17347 * #17338 * #17336 with imports fixed up to accommodate all the overlapping changes to imports. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This is the supremum of * #17376 * #17375 * #17374 * #17362 * #17355 * #17349 * #17347 * #17338 * #17336 with imports fixed up to accommodate all the overlapping changes to imports. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Quite a lot of pure order theory files import
data.set.intervals.unordered_interval
, which itself importsdata.set.intervals.image_preimage
, which in turn imports a lot of algebra.If we change the order of dependency between
data.set.intervals.unordered_interval
anddata.set.intervals.image_preimage
, we avoid algebra leaking into pure order theory and drastically reduce imports for many files.@semorrison, I expect this makes #17340 useless.