Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_ #2604

Merged
merged 10 commits into from
Mar 7, 2025
Merged

[ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_ #2604

merged 10 commits into from
Mar 7, 2025

Conversation

gallais
Copy link
Member

@gallais gallais commented Feb 20, 2025

No description provided.

JacquesCarette
JacquesCarette approved these changes Feb 20, 2025
View reviewed changes
Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice.

MatthewDaggitt
MatthewDaggitt requested changes Feb 21, 2025
View reviewed changes
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise looks good!

@jamesmckinna jamesmckinna mentioned this pull request Feb 21, 2025
Open
3 tasks
@jamesmckinna
Copy link
Contributor

Very nice!

@MatthewDaggitt MatthewDaggitt added this to the v2.3 milestone Mar 3, 2025
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Mar 3, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to a conflict with the base branch Mar 3, 2025
@gallais
Copy link
Member Author

gallais commented Mar 3, 2025 •
edited
Loading

#2631 kicked up a conflict with this PR and the principled fix is ironically to stick with what I
have and thus reverse the refactoring?!

@jamesmckinna
Copy link
Contributor

#2631 kicked up a conflict with this PR and the principled fix is ironically to stick with what I have and thus reverse the refactoring?!

I think I do not understand why this should be the 'principled' fix. One way to piggy-back on that PR is to propagate the trans refl optimisation to each of your new proofs, or have I really not understood what is going on here?

Separately (downstream, or expanding this PR?) we should perhaps consider/have already considered adding Algebra.Properties.CommutativeMonoid.Divisibility, and making that module (and CommutativeMagma/CommutativeSemigroup 'above' it) be the repository of properties of _∣_?

@gallais gallais enabled auto-merge March 7, 2025 09:57
@gallais gallais added this pull request to the merge queue Mar 7, 2025
Merged via the queue into agda:master with commit 5288e72 Mar 7, 2025
2 checks passed
@jamesmckinna jamesmckinna mentioned this pull request Mar 11, 2025
Merged
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Mar 17, 2025
@gallais @jamesmckinna
[ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_ (agda#2604
714b67f 
)

* [ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_

* [ new ] Prefix & Suffix as Left & Right division

* [ fix ] my cockup

* [ new ] ∙-cong-∣

* [ cleanup ] in the commutative case we don't care about the direction

* [ refactor ] Moving propositional results in their own module

* [ fix ] forgot the OPTIONS

* [ cleanup ] According to agda#2631

---------

Co-authored-by: jamesmckinna <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt approved these changes

@JacquesCarette JacquesCarette JacquesCarette approved these changes

Assignees
No one assigned
Labels
addition deprecation naming
Projects
None yet
Milestone
v2.3
Development

Successfully merging this pull request may close these issues.
4 participants
@gallais @jamesmckinna @JacquesCarette @MatthewDaggitt