Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(*): remove after the fact attribute [irreducible] at several places (2) #18180

Closed
wants to merge 2 commits into from

Conversation

sgouezel
Copy link
Collaborator

Part of #18164, sequel to #18168.


Open in Gitpod

@sgouezel sgouezel added awaiting-review The author would like community review of the PR mathport For compatibility with Lean 4 changes, to simplify porting labels Jan 15, 2023
@sgouezel sgouezel changed the title remove after the fact attribute [irreducible] at several places (2) chore (remove after the fact attribute [irreducible] at several places (2) Jan 15, 2023
@sgouezel sgouezel changed the title chore (remove after the fact attribute [irreducible] at several places (2) chore (*): remove after the fact attribute [irreducible] at several places (2) Jan 15, 2023
@sgouezel sgouezel changed the title chore (*): remove after the fact attribute [irreducible] at several places (2) chore(*): remove after the fact attribute [irreducible] at several places (2) Jan 15, 2023
@fpvandoorn
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 16, 2023
bors bot pushed a commit that referenced this pull request Jan 16, 2023
@bors
Copy link

bors bot commented Jan 16, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 16, 2023
@bors
Copy link

bors bot commented Jan 16, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): remove after the fact attribute [irreducible] at several places (2) [Merged by Bors] - chore(*): remove after the fact attribute [irreducible] at several places (2) Jan 16, 2023
@bors bors bot closed this Jan 16, 2023
@bors bors bot deleted the SG_more_irred branch January 16, 2023 15:58
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
mathport For compatibility with Lean 4 changes, to simplify porting ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants