Skip to content
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

chore: deprecate Array.get #7132

Merged
merged 4 commits into from
Feb 18, 2025
Merged

chore: deprecate Array.get #7132

merged 4 commits into from
Feb 18, 2025

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Feb 18, 2025

This PR moves Array.get to Array.getInternal, and adds a deprecation telling the user to use as[i] indexing notation instead. Similarly for Array.get!.

@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 18, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 11:48 Inactive
@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 Feb 18, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 18, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5bf7d4b87564960f711061df5b8491f9d24c4ed --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-18 12:04:31)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d5f565119af438b6f8ea9f5a98f3cb23c0040f5 --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-18 12:44:30)

@kim-em kim-em force-pushed the array_get_internal branch from 43c557f to 5bc3d06 Compare February 18, 2025 12:20
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 12:35 Inactive
@kim-em kim-em force-pushed the array_get_internal branch from 5bc3d06 to 55444c6 Compare February 18, 2025 21:48
@kim-em kim-em merged commit 1d9b191 into master Feb 18, 2025
10 checks passed
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 21:51 Inactive
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees
No one assigned
Labels
changes-stage0 Contains stage0 changes, merge manually using rebase 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.
2 participants
@kim-em @leanprover-community-bot