Skip to content

[Merged by Bors] - feat: port Data.Fintype.Quotient#3971

Closed
Komyyy wants to merge 6 commits intomasterfrom
port/Data.Fintype.Quotient2
Closed

[Merged by Bors] - feat: port Data.Fintype.Quotient#3971
Komyyy wants to merge 6 commits intomasterfrom
port/Data.Fintype.Quotient2

Conversation

@Komyyy
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy commented May 14, 2023 •
edited
Loading

Open in Gitpod

Komyyy added 4 commits May 14, 2023 12:25
@Komyyy
feat: port Data.Fintype.Quotient
6e76772
@Komyyy
Initial file copy from mathport
188852b
@Komyyy
automated fixes
0b7ea12 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy
fix
f1a7a1a
@Komyyy Komyyy added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. mathlib-port This is a port of a theory file from mathlib. labels May 14, 2023
@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 May 14, 2023
@Komyyy Komyyy mentioned this pull request May 14, 2023
Closed
1 task
@Komyyy Komyyy added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 14, 2023
@Parcly-Taxel Parcly-Taxel mentioned this pull request May 14, 2023
Closed
@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 May 14, 2023
@collares
Copy link
Copy Markdown
Contributor

collares commented May 22, 2023 •
edited
Loading

It seems that the related mathlib3 changes (leanprover-community/mathlib3#18417 and leanprover-community/mathlib3#19050, for example) will already require forward porting. Would it be better to forward port the whole thing once it is done?

@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented May 22, 2023

@collares It seems desirable to forward the whole thing once #18315 is merged.

@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented May 23, 2023

For the moment, I've excluded #18315 from dependents of this.

@Komyyy Komyyy removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 23, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented May 24, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 24, 2023
bors bot pushed a commit that referenced this pull request May 24, 2023
@Komyyy
feat: port Data.Fintype.Quotient (#3971)
3d4bf22
@bors
Copy link
Copy Markdown

bors bot commented May 24, 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 feat: port Data.Fintype.Quotient [Merged by Bors] - feat: port Data.Fintype.Quotient May 24, 2023
@bors bors bot closed this May 24, 2023
@bors bors bot deleted the port/Data.Fintype.Quotient2 branch May 24, 2023 11:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. 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.

3 participants

@Komyyy @collares @ChrisHughes24