Skip to content

feat: add cbv simprocs for arrays#12875

Merged
wkrozowski merged 4 commits intoleanprover:masterfrom
wkrozowski:wojciech/array_simprocs
Mar 11, 2026
Merged

feat: add cbv simprocs for arrays#12875
wkrozowski merged 4 commits intoleanprover:masterfrom
wkrozowski:wojciech/array_simprocs

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

This PR adds cbv simprocs for getting elements out of arrays.

@wkrozowski wkrozowski added the changelog-tactics User facing tactics label Mar 10, 2026
@wkrozowski
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 10, 2026

Benchmark results for 031bae0 against b626c6d are in. There are no significant changes. @wkrozowski

  • 🟥 build//instructions: +1.5G (+0.01%)

Small changes (2🟥)

  • 🟥 lake/inundation/env//task-clock: +8ms (+5.60%)
  • 🟥 lake/inundation/env//wall-clock: +9ms (+5.42%)

@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 10, 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 b626c6d326043613ba296ef9869c19148c4f4297 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 18:55:10)

@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 b626c6d326043613ba296ef9869c19148c4f4297 --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-10 18:55:11)

@wkrozowski wkrozowski marked this pull request as ready for review March 11, 2026 09:44
@wkrozowski wkrozowski requested a review from leodemoura as a code owner March 11, 2026 09:44
@wkrozowski wkrozowski enabled auto-merge March 11, 2026 09:44
@wkrozowski wkrozowski added this pull request to the merge queue Mar 11, 2026
@wkrozowski wkrozowski removed this pull request from the merge queue due to a manual request Mar 11, 2026
@wkrozowski wkrozowski added this pull request to the merge queue Mar 11, 2026
Merged via the queue into leanprover:master with commit e43b526 Mar 11, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics 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.

3 participants