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(data/list/alist): recursion on alist using insert #1724
Conversation
This needs the mathlib SHA (which would have been in the mathport file you copied from) in the header. |
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.
One of these files had an earlier pending forward-port that I've marked as dependent. Otherwise looks good.
bors d+
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
This PR/issue depends on:
|
bors merge |
Mathlib4 pair for leanprover-community/mathlib#15434 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Mathlib4 pair for leanprover-community/mathlib#15434