-
Notifications
You must be signed in to change notification settings - Fork 259
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] - chore: fix more casing errors per naming scheme #1232
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.
I haven't looked at it all, just commenting on a few that stood out to me. Feel free to open Zulip discussions in ambiguous cases.
@@ -240,7 +240,7 @@ instance (priority := 70) (R : Type _) [e : EuclideanDomain R] : NoZeroDivisors | |||
|
|||
-- see Note [lower instance priority] | |||
instance (priority := 70) (R : Type _) [e : EuclideanDomain R] : IsDomain R := | |||
{ e, NoZeroDivisors.toIsDomain R with } | |||
{ e, NoZeroDivisors.to_isDomain R with } |
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.
The to
might be a special case? See the example MonoidHom.toOneHom_injective
in the naming convention guide.
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.
My understanding is, since IsDomain
is a Prop
, to_isDomain
should follow the convention for proofs, i.e. snake case. On the other hand, toOneHom
contains data, so its name should be lower camel case.
bors merge |
I've avoided anything under `Tactic` or `test`. In correcting the names, I found `Option.isNone_iff_eq_none` duplicated between `Std` and `Mathlib`, so the `Mathlib` one has been removed. Co-authored-by: Reid Barton <rwbarton@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
I've avoided anything under
Tactic
ortest
.In correcting the names, I found
Option.isNone_iff_eq_none
duplicated betweenStd
andMathlib
, so theMathlib
one has been removed.