-
Notifications
You must be signed in to change notification settings - Fork 234
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(List/Infix): add get_tails
and get_inits
#12170
Conversation
The goal is to drop `nth_le_tails` and `nth_le_inits` soon.
Mathlib/Data/List/Infix.lean
Outdated
| zero => simp | ||
| succ n => simp [ihl] | ||
#align list.nth_le_inits List.get_inits | ||
|
||
section deprecated | ||
set_option linter.deprecated false -- TODO(Henrik): make replacements for theorems in this section |
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.
This TODO
is now done, right? The lemmas should presumably be @[deprecated $replacement]
ed.
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.
bors d+
Thanks!
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Pull request successfully merged into master. Build succeeded: |
get_tails
and get_inits
get_tails
and get_inits
The goal is to drop
nth_le_tails
andnth_le_inits
soon.Written for #9607, moved to a separate PR