-
Notifications
You must be signed in to change notification settings - Fork 235
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.
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
[Merged by Bors] - feat: port Data.List.Rdrop #1382
Conversation
b92a183
to
872b8b0
Compare
theorem rdropWhile_last_not (hl : l.rdropWhile p ≠ []) : ¬p ((rdropWhile p l).getLast hl) := by | ||
simp_rw [rdropWhile] | ||
rw [getLast_reverse] | ||
exact dropWhile_nthLe_zero_not _ _ _ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The first argument here should be 0
, I guess, but somehow it can't find that.
merge from master
…y/mathlib4 into port/Data.List.Rdrop
The theorems now all work, but it took some unpleasant rewriting of some of the proofs, largely because there's a lot of |
Nice job! Do you think it is worth replacing the |
I was also struggling to get that to work, but if we really treat |
I may have been too hasty! I looked up what people have been saying on Zulip, and there seem to be good arguments for leaving |
Maybe |
Should we do this refactor now or leave a TODO? |
@mo271 It seems that this "refactor to Boolean" is done while porting. Not ideal, but ... |
I tried to do the changes to |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>
No description provided.