Skip to content

doc: grove: update and add String data #11551

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
TwoFX merged 6 commits into from
Dec 8, 2025
Merged

doc: grove: update and add String data #11551

TwoFX merged 6 commits into from
Dec 8, 2025

Conversation

@TwoFX
Copy link
Member

@TwoFX TwoFX commented Dec 8, 2025 •
edited
Loading

This PR bumps Grove to the latest revision and starts adding data about the String library.

Just a small start, more to come.

@TwoFX TwoFX added changelog-no Do not include this PR in the release changelog grove The standard library changes in this PR should be analyzed using Grove. labels Dec 8, 2025
@TwoFX TwoFX changed the title chore: Grove: update to latest version chore: grove: update to latest version Dec 8, 2025
@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 Dec 8, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 8, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c9b8508f6b6868be1857d207edf9ac01d764f8d2 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 14:37:56)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 8, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c9b8508f6b6868be1857d207edf9ac01d764f8d2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-08 14:37:58)

@TwoFX TwoFX requested a review from kim-em as a code owner December 8, 2025 15:25
@TwoFX TwoFX changed the title chore: grove: update to latest version doc: grove: update and add String data Dec 8, 2025
@TwoFX TwoFX enabled auto-merge December 8, 2025 16:35
@TwoFX TwoFX added this pull request to the merge queue Dec 8, 2025
Merged via the queue into leanprover:master with commit 3c100ad Dec 8, 2025
15 checks passed
robsimmons pushed a commit that referenced this pull request Dec 8, 2025
@TwoFX @robsimmons
doc: grove: update and add String data (#11551)
fe18c08 
This PR bumps Grove to the latest revision and starts adding data about
the `String` library.

Just a small start, more to come.
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

changelog-no Do not include this PR in the release changelog grove The standard library changes in this PR should be analyzed using Grove. 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.

3 participants

@TwoFX @leanprover-community-bot @leanprover-bot