Skip to content

feat: another grind_pattern for getElem?_pos #11963

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
kim-em wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

feat: another grind_pattern for getElem?_pos #11963

kim-em wants to merge 4 commits into from

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Jan 10, 2026

This PR activates getElem?_pos more aggresively, triggered by c[i].

@kim-em kim-em added awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-language Language features and metaprograms labels Jan 10, 2026
kim-em and others added 3 commits January 10, 2026 07:50
@kim-em
lint exceptions
e46c971
@kim-em @claude
chore: more grind lint exceptions
da5fe54 
Add skip entries for Array.back_singleton, Array.getElem_zero_filter,
Array.getElem_zero_filterMap, and the Std.*Map.getElem_filterMap' lemmas.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@kim-em
.
43f86a2
@kim-em
Copy link
Collaborator Author

kim-em commented Jan 10, 2026

This is currently broken, because this grind_pattern causes grind? and grind => finish? etc to produce non-working scripts with many instantiate approx. Until we have better support for generating scripts which use custom grind_pattern, this probably isn't viable.

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

awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-language Language features and metaprograms

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em