Skip to content

[Merged by Bors] - feat: Filtering sups#7254

Closed
YaelDillies wants to merge 9 commits intomasterfrom
truncated_sup
Closed

[Merged by Bors] - feat: Filtering sups#7254
YaelDillies wants to merge 9 commits intomasterfrom
truncated_sup

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Sep 19, 2023 •
edited by eric-wieser
Loading

Match leanprover-community/mathlib3#18612.

The lemmas were already added in #7382, though a slight difference in the statement means that we need a new decidableExistsAndFinsetCoe instance.

Open in Gitpod

@YaelDillies YaelDillies 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 t-order Order theory labels Sep 19, 2023
@jcommelin jcommelin changed the title feat: FIltering sups feat: Filtering sups Sep 19, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 28, 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 Oct 2, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Oct 9, 2023

Please link to the mathlib3 PR in the description.

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Oct 9, 2023
@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Oct 9, 2023
eric-wieser
eric-wieser reviewed Nov 1, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 1, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Nov 1, 2023
View reviewed changes
@YaelDillies @eric-wieser
no #noalign
117bba8 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Nov 1, 2023

bors merge

Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 1, 2023
bors bot pushed a commit that referenced this pull request Nov 1, 2023
@YaelDillies
feat: Filtering sups (#7254)
4bda10c 
Match leanprover-community/mathlib3#18612.

The lemmas were already added in #7382, though a slight difference in the statement means that we need a new `decidableExistsAndFinsetCoe` instance.
@bors
Copy link
Copy Markdown

bors bot commented Nov 1, 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: Filtering sups [Merged by Bors] - feat: Filtering sups Nov 1, 2023
@bors bors bot closed this Nov 1, 2023
@bors bors bot deleted the truncated_sup branch November 1, 2023 18:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

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. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @eric-wieser