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

feat: move lemmas about lists from mathlib + add lemmas about Array.zipWith #396

Merged
merged 9 commits into from
Dec 20, 2023
Merged

feat: move lemmas about lists from mathlib + add lemmas about Array.zipWith #396

merged 9 commits into from
Dec 20, 2023

Conversation

dupuisf
Copy link
Contributor

@dupuisf dupuisf commented Nov 27, 2023

Lemmas from Mathlib.Data.List.Basic:
drop_one, drop_add, drop_left, drop_left', drop_eq_get_cons

The rest of the list lemmas are from Mathlib.Data.List.Zip.

The array lemmas are new.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 27, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 28, 2023
@semorrison semorrison added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Nov 29, 2023
@joehendrix joehendrix 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 Dec 7, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 9, 2023
@dupuisf
Copy link
Contributor Author

dupuisf commented Dec 10, 2023

awaiting-review

@github-actions github-actions bot 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 Dec 10, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 10, 2023
@joehendrix joehendrix added will-merge-soon PR will be merged soon. Any concerns should be raised quickly. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Dec 12, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 13, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 14, 2023
@joehendrix joehendrix merged commit 007a6d6 into leanprover-community:main Dec 20, 2023
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison approved these changes

@joehendrix joehendrix joehendrix approved these changes

Assignees
No one assigned
Labels
will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@dupuisf @semorrison @joehendrix @leanprover-community-mathlib4-bot