Skip to content

Conversation

@tobiasgrosser
Copy link
Contributor

No description provided.

@tobiasgrosser tobiasgrosser requested a review from kim-em as a code owner May 28, 2024 14:29
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 28, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels May 28, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented May 28, 2024

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 28, 2024
@tobiasgrosser
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label May 28, 2024
@bollu
Copy link
Contributor

bollu commented May 31, 2024

LGTM, as this was reviewed at (opencompl#4)

@kim-em kim-em removed the awaiting-review Waiting for someone to review the PR label Jun 1, 2024
@kim-em kim-em added this pull request to the merge queue Jun 1, 2024
Merged via the queue into leanprover:master with commit ff116da Jun 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants