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(algebra/add_torsor): use to_additive
for add_action
#6914
Conversation
urkud
commented
Mar 27, 2021
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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.
Really nice! Well spotted that this refactor was possible.
@@ -72,87 +60,23 @@ class add_torsor (G : out_param Type*) (P : Type*) [out_param $ add_group G] | |||
(vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g) | |||
|
|||
attribute [instance, priority 100, nolint dangerous_instance] add_torsor.nonempty | |||
|
|||
end old_structure_cmd | |||
attribute [nolint dangerous_instance] add_torsor.to_has_vsub |
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.
Why did this now appear?
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 know. This may be related to the fact that add_action
and add_torsor
don't use old_structure_cmd
anymore.
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 merge
Pull request successfully merged into master. Build succeeded: |
to_additive
for add_action
to_additive
for add_action