Skip to content

[Merged by Bors] - chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid#7503

Closed
madvorak wants to merge 4 commits intomasterfrom
cloacm
Closed

[Merged by Bors] - chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid#7503
madvorak wants to merge 4 commits intomasterfrom
cloacm

Conversation

@madvorak
Copy link
Copy Markdown
Collaborator

@madvorak madvorak commented Oct 4, 2023 •
edited
Loading

Renames:

CanonicallyOrderedMonoid ->
CanonicallyOrderedCommMonoid

CanonicallyOrderedAddMonoid ->
CanonicallyOrderedAddCommMonoid

CanonicallyLinearOrderedMonoid ->
CanonicallyLinearOrderedCommMonoid

CanonicallyLinearOrderedAddMonoid ->
CanonicallyLinearOrderedAddCommMonoid

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Oct 4, 2023

Please put the description above the --- not below it; the latter gets discarded when merged.

YaelDillies
YaelDillies reviewed Oct 4, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 4, 2023

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin
jcommelin reviewed Oct 5, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 5, 2023
bors bot pushed a commit that referenced this pull request Oct 5, 2023
@madvorak
chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid (#7503)
f3bc24c 
Renames:


`CanonicallyOrderedMonoid` ->
`CanonicallyOrderedCommMonoid`

`CanonicallyOrderedAddMonoid` ->
`CanonicallyOrderedAddCommMonoid`

`CanonicallyLinearOrderedMonoid` ->
`CanonicallyLinearOrderedCommMonoid`

`CanonicallyLinearOrderedAddMonoid` ->
`CanonicallyLinearOrderedAddCommMonoid`
@bors
Copy link
Copy Markdown

bors bot commented Oct 5, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid [Merged by Bors] - chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid Oct 5, 2023
@bors bors bot closed this Oct 5, 2023
@bors bors bot deleted the cloacm branch October 5, 2023 08:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@madvorak @eric-wieser @jcommelin @YaelDillies