-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - refactor(data/nat/lattice): move code, add lemmas #8708
Conversation
namespace enat | ||
open_locale classical | ||
|
||
noncomputable instance : complete_linear_order enat := |
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.
Does it make more sense to put this in data.nat.enat
and change the imports a bit? Or does that not work?
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.
I have no opinion here. Actually, I wanted to add nat.supr_lt_succ
etc and there was no good home for these lemmas, so I moved code around. If you want me to make data.nat.enat
import data.nat.lattice
, then I can do it. OTOH, having all *nat
(conditionally) complete lattice instances in one file makes sense too.
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.
I also don't care and don't think it matters much, just caught my eye that this was the only mention of enat
in the new file and it came at the very end. Up to you.
/-- This instance is necessary, otherwise the lattice operations would be derived via | ||
conditionally_complete_linear_order_bot and marked as noncomputable. -/ | ||
instance : lattice ℕ := lattice_of_linear_order |
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.
Should this go here?
mathlib/src/order/lattice.lean
Lines 622 to 623 in e6e5718
instance nat.distrib_lattice : distrib_lattice ℕ := | |
by apply_instance |
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.
I don't want to move more instances from files deeper in the import chain without a reason.
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.
Thanks 🎉
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
* move `nat.conditionally_complete_linear_order_with_bot` and `enat.complete_linear_order` to a new file `data.nat.lattice`; * add a few lemmas (`nat.supr_lt_succ` etc), move `set.bUnion_lt_succ` to the same file; * use `galois_insertion.lift_complete_lattice` to define `enat.complete_linear_order`.
Pull request successfully merged into master. Build succeeded: |
/-! | ||
# Conditionally complete linear order structure on `ℕ` | ||
|
||
In this file we |
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.
Can somebody fix this broken docstring?
nat.conditionally_complete_linear_order_with_bot
andenat.complete_linear_order
to a new filedata.nat.lattice
;nat.supr_lt_succ
etc), moveset.bUnion_lt_succ
to the same file;galois_insertion.lift_complete_lattice
to defineenat.complete_linear_order
.