Skip to content

fix: correct name for String.Pos.le_skipWhile#13400

Merged
TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:le_skipwhile
Apr 14, 2026
Merged

fix: correct name for String.Pos.le_skipWhile#13400
TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:le_skipwhile

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Apr 14, 2026

This PR fixes the incorrect name String.Pos.skipWhile_le to be String.Pos.le_skipWhile.

No deprecation since this is not in any release yet (also no release candidate). String.Slice.Pos.le_skipWhile is correct, as are the revSkipWhile counterparts.

@TwoFX TwoFX added the changelog-library Library label Apr 14, 2026
@TwoFX TwoFX requested a review from kim-em as a code owner April 14, 2026 06:42
@TwoFX TwoFX enabled auto-merge April 14, 2026 06:43
@TwoFX TwoFX added this pull request to the merge queue Apr 14, 2026
Merged via the queue into leanprover:master with commit d6b938d Apr 14, 2026
23 checks passed
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
This PR fixes the incorrect name `String.Pos.skipWhile_le` to be
`String.Pos.le_skipWhile`.

No deprecation since this is not in any release yet (also no release
candidate). `String.Slice.Pos.le_skipWhile` is correct, as are the
`revSkipWhile` counterparts.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant