Skip to content

feat: WF/Fix.lean: only refine fix’s ih for atomic discriminant onlys#7324

Merged
nomeata merged 9 commits intomasterfrom
joachim/wf-fix-refine-only-fvar
Mar 4, 2025
Merged

feat: WF/Fix.lean: only refine fix’s ih for atomic discriminant onlys#7324
nomeata merged 9 commits intomasterfrom
joachim/wf-fix-refine-only-fvar

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Mar 4, 2025

This PR changes the internal construction of well-founded recursion, to not change the type of fix’s induction hypothesis in non-defeq ways.

Fixes #7322 and hopefully unblocks #7166.

@nomeata nomeata added awaiting-mathlib We should not merge this until we have a successful Mathlib build merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. changelog-language Language features and metaprograms labels Mar 4, 2025
nomeata
nomeata commented Mar 4, 2025
View reviewed changes
@nomeata nomeata changed the title feat: WF/Fix.lean: Only refine fix’s ih for atomic discriminant onlys feat: WF/Fix.lean: only refine fix’s ih for atomic discriminant onlys Mar 4, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 11:19 Inactive
@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 4, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
Update lean-toolchain for testing leanprover/lean4#7324
cffa50f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2025
Update lean-toolchain for testing leanprover/lean4#7324
f266459
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build labels Mar 4, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 4, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@nomeata nomeata enabled auto-merge March 4, 2025 13:21
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 13:27 Inactive
@nomeata nomeata added this pull request to the merge queue Mar 4, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2025
Trigger CI for leanprover/lean4#7324
e6d9b39
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2025
Trigger CI for leanprover/lean4#7324
ea6aece
Merged via the queue into master with commit 23b5baa Mar 4, 2025
17 checks passed
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

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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.

Type incorrect translation of well-founded function with dite in the type

1 participant

@nomeata