-
Notifications
You must be signed in to change notification settings - Fork 243
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: Rename Dart.is_adj
to Dart.adj
#12574
Conversation
The `is` doesn't bring any information and `is_adj` really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).
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.
bors d+
I'll let you decide whether this should have a deprecation.
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
I have quite literally never heard anyone using that part of the library for anything else than the degree-sum formula, so I will claim it's fine to not deprecate🤞 bors merge |
The `is` doesn't bring any information and `is_adj` really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).
Pull request successfully merged into master. Build succeeded: |
Dart.is_adj
to Dart.adj
Dart.is_adj
to Dart.adj
The `is` doesn't bring any information and `is_adj` really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).
The `is` doesn't bring any information and `is_adj` really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).
The
is
doesn't bring any information andis_adj
really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).