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: Remove leftCoset
/rightCoset
#8877
Conversation
Those two definitions are completely obsolete now that we have the pointwise API. This PR removes them but not the corresponding API. A much more tedious subsequent PR will be needed to merge the two API.
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.
This looks great, but it's probably worth a second opinion.
Let's ask @semorrison since they authored this file... five years ago? 🧓 |
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 am in favour of merging this PR. But I think we should also make serious work of implementing notation for right actions that keeps the action visibly on the right. The version using op
will eventually lead to extremely confusing expressions, I'm quite sure.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
I agree although this is mostly orthogonal to this PR since the |
Thanks 🎉 bors merge |
Those two definitions are completely obsolete now that we have the pointwise API. This PR removes them but not the corresponding API. A much more tedious subsequent PR will be needed to merge the two API. Note that I need to tweak simp lemmas to keep confluence since I'm merging two pairs of head keys together.
Pull request successfully merged into master. Build succeeded: |
leftCoset
/rightCoset
leftCoset
/rightCoset
Those two definitions are completely obsolete now that we have the pointwise API. This PR removes them but not the corresponding API. A much more tedious subsequent PR will be needed to merge the two API. Note that I need to tweak simp lemmas to keep confluence since I'm merging two pairs of head keys together.
Those two definitions are completely obsolete now that we have the pointwise API. This PR removes them but not the corresponding API. A much more tedious subsequent PR will be needed to merge the two API.
Note that I need to tweak simp lemmas to keep confluence since I'm merging two pairs of head keys together.