Skip to content

[Merged by Bors] - feat: new file Data/List/Pi#5549

Closed
astrainfinita wants to merge 17 commits intomasterfrom
FR_list_pi
Closed

[Merged by Bors] - feat: new file Data/List/Pi#5549
astrainfinita wants to merge 17 commits intomasterfrom
FR_list_pi

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Jun 28, 2023 •
edited
Loading

The new APIs replace some definitions and lemmas in Data.FinEnum. This PR also provides more lemmas.

Open in Gitpod

@astrainfinita astrainfinita mentioned this pull request Jun 29, 2023
Closed
1 task
@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 4, 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 19, 2023
@kim-em kim-em removed the after-port label Jul 25, 2023
@kim-em kim-em mentioned this pull request Jul 27, 2023
Closed
@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 Aug 10, 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 Aug 20, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@astrainfinita astrainfinita changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 11:44
YaelDillies
YaelDillies reviewed Sep 27, 2023
View reviewed changes
@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 Oct 19, 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 20, 2023
@digama0
Copy link
Copy Markdown
Member

digama0 commented Oct 21, 2023

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

@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 Oct 31, 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 Nov 15, 2023
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2024
@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 Mar 4, 2024
@tobiasgrosser
Copy link
Copy Markdown
Contributor

tobiasgrosser commented Jun 30, 2024

@negiizhao, I am curious what the status of this PR is. Do you plan to merge this PR still?

@tobiasgrosser tobiasgrosser mentioned this pull request Jun 30, 2024
Closed
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jul 3, 2024

I'll come back to this PR when I have time. Data.Multiset.Pi and Data.Finset.Pi also don't have the module docstring so I can't fix it quickly.

@tobiasgrosser
Copy link
Copy Markdown
Contributor

tobiasgrosser commented Jul 4, 2024

OK. We had code that uses this, so merging this in would actually be pretty convenient for us.

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jul 4, 2024

@tobiasgrosser and co, maybe you can take over this PR if @negiizhao agrees?

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 24, 2024 •
edited
Loading

PR summary b097686f2d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Data.FinEnum 1
Mathlib.Data.List.Pi 399

Declarations diff

+ Pi.enum
+ Pi.finEnum
+ Pi.mem_enum
+ _root_.Multiset.Pi.cons_coe
+ _root_.Multiset.pi_coe
+ cons_def
+ cons_injective
+ cons_ne
+ cons_same
+ cons_swap
+ empty
+ head
+ mem_pi_toList
+ nil
+ pi_cons
+ pi_nil
+ tail
++ cons
++ cons_eta
++ cons_map
++ forall_rel_cons_ext
- Pi.cons_injective
- Pi.cons_ne
- Pi.cons_same
- Pi.cons_swap
- Pi.empty
- Pi.tail
- pi.cons_eta
- pi.enum
- pi.finEnum
- pi.mem_enum
-- Pi.cons

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@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 24, 2024
@astrainfinita astrainfinita removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 24, 2024
YaelDillies
YaelDillies reviewed Jul 24, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Jul 25, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm really surprised Data.List.Pi imports Data.Multiset.Pi and not the other way around. Can you explain?

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jul 25, 2024

leanprover-community/mathlib3#18417 (comment) This comment suggests redefining List.Pi.cons using Multiset.Pi.cons.

YaelDillies
YaelDillies reviewed Jul 25, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If Eric asked for it, I will trust him. The rest looks agreeable.

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 25, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 25, 2024
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 25, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 25, 2024
@astrainfinita @digama0
feat: new file Data/List/Pi (#5549)
e4bd83b 
The new APIs replace some definitions and lemmas in `Data.FinEnum`. This PR also provides more lemmas.



Co-authored-by: negiizhao <egresf@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: new file Data/List/Pi [Merged by Bors] - feat: new file Data/List/Pi Jul 25, 2024
@mathlib-bors mathlib-bors bot closed this Jul 25, 2024
@mathlib-bors mathlib-bors bot deleted the FR_list_pi branch July 25, 2024 23:15
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

7 participants

@astrainfinita @digama0 @tobiasgrosser @YaelDillies @kim-em @urkud @jcommelin