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] - style: fix references to DenselyOrdered #11897
Conversation
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.
Thank you for doing this; good find! I have two follow-up suggestions which should be quick to address.
@@ -153,15 +153,15 @@ instance denselyOrdered_of_noMaxOrder [Preorder ι] [∀ i, Preorder (α i)] | |||
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩ | |||
#align psigma.lex.densely_ordered_of_no_max_order PSigma.Lex.denselyOrdered_of_noMaxOrder | |||
|
|||
instance densely_ordered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] | |||
instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] |
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 believe the naming convention is that manual instance names should start with "inst", i.e.
instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] | |
instance instDenselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] |
(I'm not 100% sure on the casing; you may want to compare with other names/wait for another pair of eyes.)
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.
If I do this, there will be many more examples of such instances in this file alone
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.
Sure; mathlib is not always consistent (and I think a fix for that would be welcome - to be sure, I'd ask on zulip first).
I'm not asking you to change any other instances! But when you're renaming this one, I'd rather rename it to a "right" than a "less wrong" name.
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.
Personally, I would find the resulting inconsistency with e.g. denselyOrdered_of_noMaxOrder even more confusing
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
…_ordered' into sven-naming-densely_ordered
Thanks! bors merge |
Rename occurrences of "densely_ordered" to "denselyOrdered" Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Rename occurrences of "densely_ordered" to "denselyOrdered" Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Rename occurrences of "densely_ordered" to "denselyOrdered" Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Rename occurrences of "densely_ordered" to "denselyOrdered" Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Rename occurrences of "densely_ordered" to "denselyOrdered" Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Rename occurrences of "densely_ordered" to "denselyOrdered"