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

[Merged by Bors] - chore: update SHA sums #2133

Closed

urkud wants to merge 1 commit into master from YK-sha

Member

urkud commented Feb 7, 2023 •

edited by eric-wieser

Part of the List.repeat -> List.replicate refactor. On Mathlib 4 side, I removed mentions of List.repeat in #1475 and #1579


          chore: update SHA sums

1bde5e0

* [`data.list.duplicate`@`7b78d1776212a91ecc94cf601f83bdcc46b04213`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/duplicate?from=7b78d1776212a91ecc94cf601f83bdcc46b04213&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.multiset.nodup`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/multiset/nodup?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.set.pointwise.list_of_fn`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/pointwise/list_of_fn?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.multiset.bind`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/multiset/bind?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.sort`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/sort?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.nodup`@`dd71334db81d0bd444af1ee339a29298bef40734`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/nodup?from=dd71334db81d0bd444af1ee339a29298bef40734&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.pairwise`@`dd71334db81d0bd444af1ee339a29298bef40734`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/pairwise?from=dd71334db81d0bd444af1ee339a29298bef40734&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

urkud added the awaiting-review label

Member

jcommelin commented Feb 7, 2023

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

bors bot commented Feb 7, 2023

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

jcommelin added the awaiting-CI label

github-actions bot added delegated and removed awaiting-review labels

Member Author

urkud commented Feb 7, 2023

bors merge

github-actions bot added the ready-to-merge label

bors bot pushed a commit that referenced this pull request


          chore: update SHA sums (#2133)

060d1a4

Part of the `List.repeat` -> `List.replicate` refactor. On Mathlib 4 side, I removed mentions of `List.repeat` in #1475 and #1579

* [`data.list.duplicate`@`7b78d1776212a91ecc94cf601f83bdcc46b04213`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/duplicate?from=7b78d1776212a91ecc94cf601f83bdcc46b04213&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.multiset.nodup`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/multiset/nodup?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.set.pointwise.list_of_fn`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/pointwise/list_of_fn?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.multiset.bind`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/multiset/bind?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.sort`@`9003f28797c0664a49e4179487267c494477d853`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/sort?from=9003f28797c0664a49e4179487267c494477d853&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.nodup`@`dd71334db81d0bd444af1ee339a29298bef40734`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/nodup?from=dd71334db81d0bd444af1ee339a29298bef40734&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

* [`data.list.pairwise`@`dd71334db81d0bd444af1ee339a29298bef40734`..`f694c7dead66f5d4c80f446c796a5aad14707f0e`](https://leanprover-community.github.io/mathlib-port-status/file/data/list/pairwise?from=dd71334db81d0bd444af1ee339a29298bef40734&to=f694c7dead66f5d4c80f446c796a5aad14707f0e)

bors bot commented Feb 7, 2023

Pull request successfully merged into master.

Build succeeded:

Build
Lint style

bors bot changed the title ~~chore: update SHA sums~~ [Merged by Bors] - chore: update SHA sums

bors bot closed this

bors bot deleted the YK-sha branch

February 7, 2023 07:58

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment