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: getElem_tail lemmas #905

Merged
merged 17 commits into from
Sep 28, 2024
Merged

feat: getElem_tail lemmas #905

merged 17 commits into from
Sep 28, 2024

Conversation

pimotte
Copy link
Contributor

@pimotte pimotte commented Aug 3, 2024

I felt like these were missing, I tried adhering to the existing standards, but happy to patch things up if I missed something:)

@pimotte
Copy link
Contributor Author

pimotte commented Aug 3, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Aug 3, 2024
fgdorais
fgdorais requested changes Aug 3, 2024
View reviewed changes
Batteries/Data/List/Lemmas.lean Outdated Show resolved Hide resolved
Batteries/Data/List/Lemmas.lean Outdated Show resolved Hide resolved
Batteries/Data/List/Lemmas.lean Outdated Show resolved Hide resolved
Batteries/Data/List/Lemmas.lean Outdated Show resolved Hide resolved
pimotte and others added 2 commits August 4, 2024 10:36
@pimotte @fgdorais
Update Batteries/Data/List/Lemmas.lean
f9ec3fa 
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
@pimotte
Post-review fixes
0888c7d
@pimotte pimotte requested a review from fgdorais August 4, 2024 08:45
@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 Aug 5, 2024
@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 Aug 5, 2024
@fgdorais
Copy link
Collaborator

fgdorais commented Aug 5, 2024 •
edited
Loading

There is an unresolved "missing simp" issue here but the author and I resolved that this is probably not the right place to fix that problem.

@fgdorais fgdorais requested a review from digama0 August 5, 2024 19:01
@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 Aug 17, 2024
@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 Aug 25, 2024
@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 Sep 3, 2024
@kim-em kim-em 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. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Sep 9, 2024
@fgdorais fgdorais 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 Sep 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 28, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#905
69d15a5
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@fgdorais fgdorais mentioned this pull request Sep 28, 2024
Closed
@fgdorais
Copy link
Collaborator

Mathlib adaptation #17229

@fgdorais fgdorais added this pull request to the merge queue Sep 28, 2024
Merged via the queue into leanprover-community:main with commit 82c92a6 Sep 28, 2024
2 checks passed
fgdorais pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 28, 2024
@leanprover-community-mathlib4-bot @fgdorais
Update Batteries branch for testing leanprover-community/batteries#905
fb68d0f
fgdorais added a commit that referenced this pull request Oct 1, 2024
@pimotte @fgdorais @kim-em
feat: getElem_tail lemmas (#905)
33d0f47 
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@fgdorais fgdorais fgdorais approved these changes

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@pimotte @fgdorais @leanprover-community-bot @kim-em @leanprover-community-mathlib4-bot