Skip to content

fix: more realizeConst fixes#7300

Merged
Kha merged 3 commits intoleanprover:masterfrom
Kha:push-qwrxopwotlls
Mar 3, 2025
Merged

fix: more realizeConst fixes#7300
Kha merged 3 commits intoleanprover:masterfrom
Kha:push-qwrxopwotlls

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Mar 3, 2025

Found and debugged while working on stage 2 of #7247

@Kha Kha added the changelog-no Do not include this PR in the release changelog label Mar 3, 2025
@Kha Kha requested a review from leodemoura as a code owner March 3, 2025 10:48
@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 3, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 3, 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 9c47f395c8724b105659d0aa537dd675b29f76aa --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 11:13:08)

@Kha Kha added this pull request to the merge queue Mar 3, 2025
Merged via the queue into leanprover:master with commit 0a55f4b Mar 3, 2025
17 checks passed
@Kha Kha deleted the push-qwrxopwotlls branch March 3, 2025 12:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

Assignees

No one assigned

Labels

changelog-no Do not include this PR in the release changelog 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.

1 participant

@Kha