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: partial calc tactic would fail due to mdata or uninstantiated mvars #4335

Merged
merged 2 commits into from
Jun 4, 2024
Merged

fix: partial calc tactic would fail due to mdata or uninstantiated mvars #4335

merged 2 commits into from
Jun 4, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Jun 4, 2024

Reported by Heather Macbeth.

Closes #4334

@kmill kmill requested a review from semorrison as a code owner June 4, 2024 00:08
@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 Jun 4, 2024
@leanprover-community-mathlib4-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 f65e3ae9859a4288b94b4a9fda93f406244d8dbc --onto 81f5b07215b077f9b5be677f8689617512d3322c. (2024-06-04 00:27:00)

@semorrison semorrison added this pull request to the merge queue Jun 4, 2024
hrmacbeth
hrmacbeth reviewed Jun 4, 2024
View reviewed changes
tests/lean/run/4334.lean Outdated Show resolved Hide resolved
@kmill kmill removed this pull request from the merge queue due to a manual request Jun 4, 2024
@kmill @hrmacbeth
spelling
3d6b658 
Co-authored-by: Heather Macbeth <[email protected]>
@kmill kmill enabled auto-merge June 4, 2024 01:07
@kmill kmill added this pull request to the merge queue Jun 4, 2024
Merged via the queue into leanprover:master with commit a54fa7c Jun 4, 2024
11 checks passed
Komyyy pushed a commit to Komyyy/lean4 that referenced this pull request Jun 4, 2024
@kmill @hrmacbeth @Komyyy
fix: partial calc tactic would fail due to mdata or uninstantiated …
37dccb1 
…mvars (leanprover#4335)

Reported by Heather Macbeth.

Closes leanprover#4334

---------

Co-authored-by: Heather Macbeth <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hrmacbeth hrmacbeth hrmacbeth left review comments

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

Assignees
No one assigned
Labels
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.

partial calc affected by tactics preceding it
3 participants
@kmill @leanprover-community-mathlib4-bot @hrmacbeth