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: improve error message when termination argument is too dependent #3414

Merged
merged 4 commits into from
Feb 22, 2024
Merged

fix: improve error message when termination argument is too dependent #3414

merged 4 commits into from
Feb 22, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 20, 2024

this may help users when they face #2260

fixes #2260

@nomeata nomeata mentioned this pull request Feb 20, 2024
Closed
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 20, 2024 10:37 Inactive
@nomeata nomeata requested a review from leodemoura February 20, 2024 10:40
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 20, 2024 10:47 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 20, 2024 11:00 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 20, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 20, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3414
3fcfbb7
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 20, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3414
a73e6c5
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 20, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Feb 20, 2024 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 20, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3414
2a187d2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 20, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3414
8204b51
@nomeata
Revert "grammar"
5683b0e 
This reverts commit bddb56d.
@nomeata nomeata enabled auto-merge February 22, 2024 16:19
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 22, 2024 16:32 Inactive
@nomeata nomeata added this pull request to the merge queue Feb 22, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3414
9a0bc65
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3414
d81035a
Merged via the queue into master with commit 5bbc544 Feb 22, 2024
11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@david-christiansen david-christiansen david-christiansen left review comments

@leodemoura leodemoura Awaiting requested review from leodemoura

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
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

termination_by fails with dependent matching
3 participants
@nomeata @leanprover-community-mathlib4-bot @david-christiansen