Skip to content

[Merged by Bors] - chore: add a Repr for Sym2#14251

Closed
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/Sym2-Repr
Closed

[Merged by Bors] - chore: add a Repr for Sym2#14251
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/Sym2-Repr

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

This matches the approach used by Multiset


Open in Gitpod

This matches the approach used by `Multiset`
@eric-wieser eric-wieser added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 29, 2024
@eric-wieser eric-wieser requested a review from kmill June 29, 2024 01:09
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 29, 2024

PR summary 57a51a7981

Import changes

No significant changes to the import graph


Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 29, 2024
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

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 10, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 10, 2024
This matches the approach used by `Multiset`
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 10, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: add a Repr for Sym2 [Merged by Bors] - chore: add a Repr for Sym2 Jul 10, 2024
@mathlib-bors mathlib-bors bot closed this Jul 10, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/Sym2-Repr branch July 10, 2024 08:42
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants