Skip to content

feat: grind annotations for List/Array/Vector.finRange theorems #8747

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
Merged
kim-em merged 1 commit into from
Jun 12, 2025
Merged

feat: grind annotations for List/Array/Vector.finRange theorems #8747

kim-em merged 1 commit into from
Jun 12, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Jun 12, 2025 •
edited
Loading

This PR adds grind annotations for `List/Array/Vector.finRange` theorems.

@kim-em kim-em added the changelog-library Library label Jun 12, 2025
@kim-em kim-em enabled auto-merge June 12, 2025 17:26
@kim-em kim-em force-pushed the feat/grind-annotations-finrange branch from c0c897d to e6f71a0 Compare June 12, 2025 17:26
@kim-em kim-em changed the title feat: grind annotations for Array/Vector.finRange theorems feat: grind annotations for List/Array/Vector.finRange theorems Jun 12, 2025
@kim-em kim-em added this pull request to the merge queue Jun 12, 2025
@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 Jun 12, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jun 12, 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 f0347ee719abfbbe27159ebf896877411966f5bf --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 18:08:15)

Merged via the queue into master with commit 75fe50a Jun 12, 2025
17 checks passed
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@kim-em @algebraic-dev
feat: grind annotations for List/Array/Vector.finRange theorems (lean…
4b615c9 
…prover#8747)

This PR adds grind annotations for \`List/Array/Vector.finRange\`
theorems.
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@kim-em @wkrozowski
feat: grind annotations for List/Array/Vector.finRange theorems (lean…
41d5fb6 
…prover#8747)

This PR adds grind annotations for \`List/Array/Vector.finRange\`
theorems.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-library Library 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.

3 participants

@kim-em @leanprover-community-bot