Skip to content

refactor: rename ForwardPattern.dropPrefix? to ForwardPattern.skipPrefix?#12984

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

refactor: rename ForwardPattern.dropPrefix? to ForwardPattern.skipPrefix?#12984
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:dropprefix

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 19, 2026

This PR renames the function ForwardPattern.dropPrefix? to ForwardPattern.skipPrefix?

This function (s : String.Slice) -> Option s.Pos is not to be confused with String.Slice.dropPrefix? : (s : String.Slice) -> Option String.Slice.

@TwoFX TwoFX requested a review from kim-em as a code owner March 19, 2026 12:55
@TwoFX TwoFX added the changelog-library Library label Mar 19, 2026
@TwoFX TwoFX changed the title chore: rename ForwardPattern.dropPrefix? to ForwardPattern.skipPrefix? refactor: rename ForwardPattern.dropPrefix? to ForwardPattern.skipPrefix? Mar 19, 2026
@TwoFX TwoFX enabled auto-merge March 19, 2026 12:55
@TwoFX TwoFX added this pull request to the merge queue Mar 19, 2026
Merged via the queue into leanprover:master with commit 9c5d2bf Mar 19, 2026
23 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 8f6ade06ea2964d55625a9809f3349a0112aee04 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 13:45:29)

@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 8f6ade06ea2964d55625a9809f3349a0112aee04 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 13:45:31)

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