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.

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

refactor: simpMatch to not etaStruct #6901

Merged
merged 2 commits into from
Feb 1, 2025
Merged

refactor: simpMatch to not etaStruct #6901

merged 2 commits into from
Feb 1, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 1, 2025 •
edited
Loading

This PR changes the simpMatch function, used inside the equation generator for WF-rec functions, to not do eta-expansion.

This makes the process a bit more robust and disciplined, and avoids removing match-statements (and introduce projections and dependencies) that we'd rather split instead.

Also adds more tracing to the equational theorem generator.

Extracted from #6898.

@nomeata
refactor: simpMatch to not etaStruct
32caf9a 
This PR changes the `simpMatch` function, used inside the equation generator for
WF-rec functions, to not do eta-expansion.

This makes the process a bit more robust and disciplined, and avoids removing
match-statements (and introduce projections and dependencies) that we'd rather
split instead.
@nomeata nomeata added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Feb 1, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 16:28 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 Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6901
ec270c6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6901
ba82098
@leanprover-community-bot leanprover-community-bot removed the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Feb 1, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 1, 2025 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 1, 2025
@nomeata nomeata marked this pull request as ready for review February 1, 2025 17:31
@nomeata nomeata requested a review from leodemoura as a code owner February 1, 2025 17:31
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 1, 2025 17:38 Inactive
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Feb 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6901
1661a73
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 1, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6901
62492bb
@nomeata nomeata added this pull request to the merge queue Feb 1, 2025
Merged via the queue into master with commit deb3299 Feb 1, 2025
19 checks passed
This was referenced Feb 4, 2025
Open
Closed
nomeata added a commit that referenced this pull request Feb 4, 2025
@nomeata
test: more equational theorem generation tests
cf4b3dc 
This includes the examples from issues #2961, #3219 and #5667 in our
test suite, so that we know when (accidentially) fix them.

In fact this closes #3219, which (judging from the nightlies) was fixed
last week by #6901.
@nomeata nomeata mentioned this pull request Feb 4, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Feb 4, 2025
@nomeata
test: more equational theorem generation tests (#6952)
33baacc 
This includes the examples from issues #2961, #3219 and #5667 in our
test suite, so that we know when (accidentially) fix them.

In fact this closes #3219, which (judging from the nightlies) was fixed
last week by #6901.
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
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-bot