[Merged by Bors] - feat: list lemmas #11626
Conversation
sven-manthe
added
awaiting-review
There was a problem hiding this comment.
Thanks for your contribution and welcome to mathlib!
I gave your PR a first look and have a lot of style comments. (This is perfectly normed for a first PR.) Quite a few things are also copied from the style guide; did you get to read that already?
Some issues occur several times - I haven't mentioned them all the time; please also address similar instances below.
grunweg
added
awaiting-author
|
Thank you. I had a look at the style guide already, but my attempts to fix this with a few regexps didn't find all the issues. Now, apart from "hypotheses left of colon" (see above), I tried to fix all the mentioned issues |
sven-manthe
added
awaiting-review
|
One more thing: when you're addressed a comment, can you click "resolve conversation"? (If you would still like some opinion on a question, just leave it open. But right now, it's hard to see which is which.) Thanks! Update: I just did this for most of them. |
grunweg
added
awaiting-author
|
sven-manthe
added
awaiting-review
I know! For me, it was easier to fix them all - I added you as a co-author on #11714. (Feel free to tweak how you're mentioned in the PR description.) I hope that's also fine! |
leanprover-community-mathlib4-bot
added
the
merge-conflict
fpvandoorn
added
awaiting-author
|
Also, please merge master because there is a merge conflict. Let me know if you need help / need me to do it. |
suggested changes, added ext_iff
sven-manthe
added
awaiting-review
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
sven-manthe
added
awaiting-review
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
leanprover-community-mathlib4-bot
added
ready-to-merge
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
|
Build failed (retrying...): |
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext. Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>
Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext.
These lemmas are used in a project on Borel determinacy that may be added to mathlib.