Skip to content

[Merged by Bors] - feat: make Dfinsupp.sigmaCurry computable#1947

Closed
astrainfinita wants to merge 5 commits intomasterfrom
FR_dfinsupp_sigma_curry
Closed

[Merged by Bors] - feat: make Dfinsupp.sigmaCurry computable#1947
astrainfinita wants to merge 5 commits intomasterfrom
FR_dfinsupp_sigma_curry

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Jan 30, 2023 •
edited
Loading

@astrainfinita astrainfinita added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 30, 2023
@astrainfinita astrainfinita mentioned this pull request Jan 30, 2023
Closed
@astrainfinita astrainfinita removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 30, 2023
@astrainfinita astrainfinita added after-port and removed mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Feb 13, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 3, 2023
@astrainfinita astrainfinita removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 29, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 12, 2023
@kim-em kim-em removed the after-port label Jul 25, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 31, 2023
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Aug 10, 2023

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 10, 2023
bors bot pushed a commit that referenced this pull request Aug 10, 2023
@astrainfinita
feat: make Dfinsupp.sigmaCurry computable (#1947)
8c390f6 
~~mathlib3 PR: leanprover-community/mathlib3#18316
@bors
Copy link
Copy Markdown

bors bot commented Aug 10, 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: make Dfinsupp.sigmaCurry computable [Merged by Bors] - feat: make Dfinsupp.sigmaCurry computable Aug 10, 2023
@bors bors bot closed this Aug 10, 2023
@bors bors bot deleted the FR_dfinsupp_sigma_curry branch August 10, 2023 11:36
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@astrainfinita @kim-em
feat: make Dfinsupp.sigmaCurry computable (#1947)
7c3766f 
~~mathlib3 PR: leanprover-community/mathlib3#18316
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@astrainfinita @kim-em
feat: make Dfinsupp.sigmaCurry computable (#1947)
4501556 
~~mathlib3 PR: leanprover-community/mathlib3#18316
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

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

@astrainfinita @ocfnash @kim-em