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

fix: issues #2669 #2281 #2734

Merged
merged 7 commits into from
Oct 25, 2023
Merged

fix: issues #2669 #2281 #2734

merged 7 commits into from
Oct 25, 2023

Conversation

leodemoura
Copy link
Member

@semorrison This PR fixes a high priority issue, but will probably break user-defined functions that manipulate discrimination trees.

This commit also removes parameter `simpleReduce` from discrimination
trees, and take WHNF configuration options.
Reason: it is more dynamic now. For example, the simplifier
will be able to use different configurations for discrimination tree insertion
and retrieval. We need this feature to address issues #2669 and #2281

This commit also removes the dead Meta.Config field `zetaNonDep`.
@leodemoura
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit bc03c21.
There were no significant changes against commit 52f1000.

@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 Oct 22, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 22, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 22, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Oct 22, 2023

kim-em added a commit to leanprover-community/batteries that referenced this pull request Oct 23, 2023
kim-em added a commit to leanprover-community/aesop that referenced this pull request Oct 23, 2023
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 23, 2023
@kim-em kim-em linked an issue Oct 23, 2023 that may be closed by this pull request
Co-authored-by: Scott Morrison <[email protected]>

Co-authored-by: Scott Morrison <[email protected]>

Co-authored-by: Scott Morrison <[email protected]>
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 23, 2023
Given a local context containing `x : t := e`,
`simp (config := { zeta := false }) [x]` will expand `x` even
if `zeta := false`.
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 24, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 24, 2023
@leodemoura leodemoura merged commit dbcc796 into master Oct 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Projects
None yet
Development

Successfully merging this pull request may close these issues.

RFC: simp should not reduce tactic-defined lets.
4 participants