Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Std bump for std4#99 #6575

Closed
wants to merge 11 commits into from
Closed

Std bump for std4#99 #6575

wants to merge 11 commits into from

Conversation

JamesGallicchio
Copy link
Collaborator

Open in Gitpod

@JamesGallicchio JamesGallicchio changed the title Std bump/pr 99 Std bump for std4#99 Aug 14, 2023
@JamesGallicchio JamesGallicchio mentioned this pull request Aug 14, 2023
Merged
fgdorais
fgdorais reviewed Aug 14, 2023
View reviewed changes
Copy link
Collaborator

@fgdorais fgdorais left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Using @ makes things hard to maintain. So I think the appropriate fix here is to write a better proof rather than updating the _ pattern.

PS: Oops! I thought this would be a located comment! I'm referring to the error at "Mathlib/Data/List/Nodup.lean:181:44"

@JamesGallicchio JamesGallicchio force-pushed the std-bump/pr-99 branch 3 times, most recently from 0d65227 to c4f94a9 Compare August 17, 2023 00:57
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 17, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 22, 2023
@semorrison semorrison mentioned this pull request Aug 22, 2023
Closed
@semorrison
Copy link
Contributor

Rolled into #6721.

@semorrison semorrison closed this Aug 22, 2023
bors bot pushed a commit that referenced this pull request Aug 23, 2023
@semorrison @JamesGallicchio
chore: bump Std (#6721)
f59eee0 
This incorporates changes from #6575

I have also renamed `Multiset.countp` to `Multiset.countP` for consistency.

Co-authored-by: James Gallichio <jamesgallicchio@gmail.com>




Co-authored-by: James <jamesgallicchio@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fgdorais fgdorais fgdorais left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@JamesGallicchio @semorrison @fgdorais @leanprover-community-mathlib4-bot