Skip to content

[Merged by Bors] - feat: attach and filter lemmas#1470

Closed
YaelDillies wants to merge 3 commits intomasterfrom
count_attach
Closed

[Merged by Bors] - feat: attach and filter lemmas#1470
YaelDillies wants to merge 3 commits intomasterfrom
count_attach

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jan 10, 2023

@YaelDillies YaelDillies added the mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged label Jan 10, 2023
@YaelDillies YaelDillies mentioned this pull request Jan 10, 2023
Closed
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) forward-port-placeholder and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Mar 26, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:18
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Nov 3, 2023

This one is now ready to be ported

@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. forward-port-placeholder labels Nov 4, 2023
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Nov 8, 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 Nov 8, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
d36f6a1 
Match leanprover-community/mathlib3#18087
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 8, 2023

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
ffda3f2 
Match leanprover-community/mathlib3#18087
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 8, 2023

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
929a39d 
Match leanprover-community/mathlib3#18087
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 8, 2023

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
92d78f8 
Match leanprover-community/mathlib3#18087
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 8, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: attach and filter lemmas [Merged by Bors] - feat: attach and filter lemmas Nov 8, 2023
@mathlib-bors mathlib-bors bot closed this Nov 8, 2023
@mathlib-bors mathlib-bors bot deleted the count_attach branch November 8, 2023 23:58
grunweg pushed a commit that referenced this pull request Dec 15, 2023
@YaelDillies @grunweg
feat: attach and filter lemmas (#1470)
4e2de98 
Match leanprover-community/mathlib3#18087
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

mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.

Projects

No open projects
Forward ports of mathlib3
Status: Awaiting mathlib3 review

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @eric-wieser @fpvandoorn @kim-em