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

chore: de-mathlib List.Perm #89

Merged
merged 50 commits into from
Dec 8, 2023
Merged

chore: de-mathlib List.Perm #89

merged 50 commits into from
Dec 8, 2023

Conversation

JamesGallicchio
Copy link
Collaborator

@JamesGallicchio JamesGallicchio commented Jan 19, 2023 •
edited
Loading

Depends on #100.

@JamesGallicchio JamesGallicchio marked this pull request as ready for review January 26, 2023 22:02
Vtec234
Vtec234 reviewed Jan 26, 2023
View reviewed changes
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Vtec234
Vtec234 reviewed Jan 26, 2023
View reviewed changes
Std/Data/HashMap/WF.lean Outdated Show resolved Hide resolved
Vtec234
Vtec234 reviewed Jan 26, 2023
View reviewed changes
Std/Logic.lean Outdated Show resolved Hide resolved
Vtec234
Vtec234 reviewed Jan 30, 2023
View reviewed changes
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
@JamesGallicchio
Copy link
Collaborator Author

Splitting into smaller PRs (with contents identical to the PR as of closing this)

fgdorais
fgdorais requested changes Nov 22, 2023
View reviewed changes
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
@fgdorais fgdorais added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Nov 22, 2023
@JamesGallicchio
Copy link
Collaborator Author

Based on the Mathlib patch (here), ~all the breakage is from

  • making ~ et al notations scoped to the List namespace
  • lemmas using \forall {a b}, R a b -> R b a instead of Symmetric R (which is not in Std)

fgdorais
fgdorais requested changes Nov 23, 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.

Clarified style changes.

PS: I didn't expect gh to format these comments this way... Confusing!

Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
@JamesGallicchio JamesGallicchio added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Nov 24, 2023
fgdorais
fgdorais approved these changes Nov 24, 2023
View reviewed changes
Copy link
Collaborator

@fgdorais fgdorais left a comment

Choose a reason for hiding this comment

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

Looks good to me! Since I don't use Perm much, a second set of eyes is recommended.

Just a few small style suggestions. None are required, I approve anyway.

Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
Std/Data/List/Perm.lean Outdated Show resolved Hide resolved
@digama0 digama0 added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label Dec 7, 2023
@joehendrix joehendrix removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. will-merge-soon PR will be merged soon. Any concerns should be raised quickly. labels Dec 8, 2023
@joehendrix joehendrix merged commit 63c387d into leanprover-community:main Dec 8, 2023
1 check passed
@eric-wieser eric-wieser mentioned this pull request Dec 8, 2023
Closed
3 tasks
@semorrison semorrison mentioned this pull request Dec 10, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill left review comments

@Vtec234 Vtec234 Vtec234 left review comments

@digama0 digama0 digama0 approved these changes

@joehendrix joehendrix joehendrix approved these changes

@fgdorais fgdorais fgdorais approved these changes

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
8 participants
@JamesGallicchio @semorrison @Vtec234 @kmill @digama0 @joehendrix @fgdorais @leanprover-community-mathlib4-bot