Skip to content

feat: verify String.startsWith and String.skipPrefix?#12990

Merged
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:dropprefix-4
Mar 19, 2026
Merged

feat: verify String.startsWith and String.skipPrefix?#12990
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:dropprefix-4

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 19, 2026

This PR verifies the String.startsWith and String.skipPrefix? functions for our various pattern types.

@TwoFX TwoFX requested a review from kim-em as a code owner March 19, 2026 17:54
@TwoFX TwoFX added the changelog-library Library label Mar 19, 2026
@TwoFX TwoFX enabled auto-merge March 19, 2026 17:54
@TwoFX TwoFX added this pull request to the merge queue Mar 19, 2026
Merged via the queue into leanprover:master with commit 34cf457 Mar 19, 2026
21 checks passed
@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 19, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 18:45:14)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 18:45:15)

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

Labels

changelog-library Library 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.

2 participants