Skip to content

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

Closed
urkud wants to merge 1 commit intomasterfrom
YK-sha
Closed

[Merged by Bors] - chore: update SHA sums#2133
urkud wants to merge 1 commit intomasterfrom
YK-sha

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Feb 7, 2023 •
edited by eric-wieser
Loading

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

Open in Gitpod

@urkud
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)
@jcommelin
Copy link
Copy Markdown
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
Copy link
Copy Markdown

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 jcommelin added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 7, 2023
@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 7, 2023
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Feb 7, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 7, 2023
bors bot pushed a commit that referenced this pull request Feb 7, 2023
@urkud
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
Copy link
Copy Markdown

bors bot commented Feb 7, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: update SHA sums [Merged by Bors] - chore: update SHA sums Feb 7, 2023
@bors bors bot closed this Feb 7, 2023
@bors 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

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@urkud @jcommelin