-
Notifications
You must be signed in to change notification settings - Fork 242
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
Fix #2396 by removing redundant zero in IsNonAssociativeRing #2410
base: master
Are you sure you want to change the base?
Conversation
Thanks for the speedy follow-up on the issue... but the failing CI tests show that replacing the (redundant) explicit field with a definition/manifest field is Issues:
|
Thanks for reviewing this so quickly! I was about to mark the PR as a draft to fix the usage of About the change being |
I'd definitely go with DRAFT for the time being... |
Sounds like a plan! |
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.
Approving these changes "on their own" but agree with @jamesmckinna about the breaking aspects.
The zero field in the IsNonAssociativeRing was redundant, and could be replaced with a proof based on the other properties.
Now that we've replaced the field `zero` with a definition, we need to update the usages of `IsNonAssociativeRing`.
23b7da7
to
07cae12
Compare
Re: the discussion on #2396 I'd be tempted to take this off |
For the removal of the redundant `zero` parameter in `IsNonAssociativeRing`.
@jamesmckinna Updated the PR to be 'ready to go'. I'll tackle the almighty |
The zero field in the IsNonAssociativeRing was redundant, and could be replaced with a proof based on the other properties.