Skip to content
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

fix: doc in List.removeAll #7288

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix: doc in List.removeAll #7288

wants to merge 1 commit into from

Conversation

Seasawher
Copy link
Contributor

@Seasawher Seasawher requested a review from kim-em as a code owner March 2, 2025 12:11
@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 Mar 2, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3f98b4835c434c0319bd16feadb6f77239813eb5 --onto a86145b6bb2669e8864b04ef3f286dc57a4aaef0. (2025-03-02 12:42:07)

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

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Seasawher @leanprover-community-bot