Skip to content
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.

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

feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems #7261

Open
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

Kha
Copy link
Member

@Kha Kha commented Feb 27, 2025

This PR ensures all equation, unfold, induction, and partial fixpoint theorem generators in core are compatible with parallelism.

Stacked on #7247

@Kha Kha added the changelog-language Language features, tactics, and metaprograms label Feb 27, 2025
@Kha Kha requested a review from tydeu as a code owner February 27, 2025 20:31
@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 Feb 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 27, 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 2e66341f69a0db9ef8b8e5255d0f0cfa73cdadc1 --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-27 21:00:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-28 16:24:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto a86145b6bb2669e8864b04ef3f286dc57a4aaef0. (2025-03-02 13:51:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 10:35:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e7a411a66df1c3f83d3499891616770851e4e5be --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 12:42:10)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a55f4bf363843b262ea04cdc0137f125d616ff4 --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 13:17:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a244b0688244a0b9036fc2f14e63c1368bbdd94c --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 13:47:39)

@Kha Kha force-pushed the push-mmmvwovluvul branch from 0933ec6 to bc66ac0 Compare February 28, 2025 09:28
@Kha Kha added this pull request to the merge queue Feb 28, 2025
@Kha Kha removed this pull request from the merge queue due to a manual request Feb 28, 2025
@Kha Kha force-pushed the push-mmmvwovluvul branch 2 times, most recently from a998c79 to 7670c44 Compare February 28, 2025 15:57
@Kha Kha requested a review from leodemoura as a code owner February 28, 2025 15:57
@Kha Kha changed the title feat: use realizeConst for all equation theorems feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems Feb 28, 2025
@Kha Kha force-pushed the push-mmmvwovluvul branch 5 times, most recently from 386621f to 16b3759 Compare March 3, 2025 13:18
@Kha Kha force-pushed the push-mmmvwovluvul branch from 16b3759 to 7de8c9c Compare March 3, 2025 15:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-language Language features, tactics, and metaprograms 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.

2 participants