Skip to content

fix: use realizeGlobalConstNoOverloadWithInfo for grind_pattern elaboration #10427

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
Closed
Rob23oba wants to merge 1 commit into from
Closed

fix: use realizeGlobalConstNoOverloadWithInfo for grind_pattern elaboration #10427

Rob23oba wants to merge 1 commit into from

Conversation

@Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Sep 17, 2025 •
edited
Loading

This PR fixes the grind_pattern command to realize constants.

Closes #10426

@Rob23oba Rob23oba requested a review from kim-em as a code owner September 17, 2025 12:22
@github-actions github-actions bot added changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Sep 17, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Sep 17, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-17 13:27:40)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Sep 17, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-17 13:27:42)

@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Sep 30, 2025
leodemoura added a commit that referenced this pull request Oct 26, 2025
@leodemoura
chore: use realizeGlobalConstNoOverloadWithInfo
879c93f 
closes #10427
closes #10426
@leodemoura leodemoura mentioned this pull request Oct 26, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Oct 26, 2025
@leodemoura
chore: use realizeGlobalConstNoOverloadWithInfo (#10963)
93c5bd0 
closes #10427
closes #10426
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
@leodemoura @wkrozowski
chore: use realizeGlobalConstNoOverloadWithInfo (leanprover#10963)
5558aef 
closes leanprover#10427
closes leanprover#10426
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms P-low We are not planning to work on this issue 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.

grind_pattern command doesn't cause realizations

3 participants

@Rob23oba @leanprover-community-bot @leanprover-bot