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

fix: simp_all? local declarations #6385

Merged
merged 1 commit into from
Dec 14, 2024
Merged

fix: simp_all? local declarations #6385

merged 1 commit into from
Dec 14, 2024

Conversation

leodemoura
Copy link
Member

This PR fixes a bug in simp_all? that caused some local declarations to be omitted from the Try this: suggestions.

closes #3519

@leodemoura
fix: simp_all? local declarations
abd4495 
This PR fixes a bug in `simp_all?` that caused some local declarations to be omitted from the `Try this:` suggestions.

closes #3519
@leodemoura leodemoura added the changelog-language Language features, tactics, and metaprograms label Dec 14, 2024
@leodemoura leodemoura requested a review from digama0 as a code owner December 14, 2024 22:54
@leodemoura leodemoura enabled auto-merge December 14, 2024 22:54
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 14, 2024 23:01 Inactive
@leodemoura leodemoura added this pull request to the merge queue Dec 14, 2024
@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 Dec 14, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b721c0f54041f6a6adc618c07851a7e0414bd1e4 --onto bac34c7767bcf11ee80f40afcea03d80cee316f6. (2024-12-14 23:17:04)

Merged via the queue into master with commit 94641e8 Dec 14, 2024
18 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@leodemoura @luisacicolini
fix: simp_all? local declarations (leanprover#6385)
afd0d39 
This PR fixes a bug in `simp_all?` that caused some local declarations
to be omitted from the `Try this:` suggestions.

closes leanprover#3519
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@leodemoura @JovanGerb
fix: simp_all? local declarations (leanprover#6385)
587756b 
This PR fixes a bug in `simp_all?` that caused some local declarations
to be omitted from the `Try this:` suggestions.

closes leanprover#3519
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

Assignees
No one assigned
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

simp_all? omits unfolded let hypotheses
2 participants
@leodemoura @leanprover-community-bot