Skip to content

feat: suggestions for some size/count/length confusions #11588

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
Draft
robsimmons wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

feat: suggestions for some size/count/length confusions #11588

robsimmons wants to merge 1 commit into from

Conversation

@robsimmons
Copy link
Contributor

@robsimmons robsimmons commented Dec 10, 2025

This PR adds suggest_for annotations directing uses of Array.length permanently to Array.size, and uses of String.size permanently to String.length.

@robsimmons robsimmons added the changelog-language Language features and metaprograms label Dec 10, 2025
@robsimmons
Copy link
Contributor Author

robsimmons commented Dec 10, 2025

(Note: only merge after #11554)

@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 10, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 10, 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 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 14:59:50)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 10, 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 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-10 14:59:52)

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

Reviewers

@datokrat datokrat Awaiting requested review from datokrat datokrat will be requested when the pull request is marked ready for review datokrat is a code owner

@david-christiansen david-christiansen Awaiting requested review from david-christiansen david-christiansen will be requested when the pull request is marked ready for review david-christiansen is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms 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.

4 participants

@robsimmons @leanprover-community-bot @leanprover-bot