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

feat: termination_by? #3514

Merged
merged 6 commits into from
Feb 28, 2024
Merged

feat: termination_by? #3514

merged 6 commits into from
Feb 28, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 27, 2024 •
edited
Loading

the user can now write termination_by? to see the termination argument
inferred by GuessLex, and turn it into termination_by … using the “Try
this” widget or a code action.

To be done later, maybe: Avoid writing sizeOf if it's not necessary.

@nomeata
feat: termination_by?
a24a777 
the user can now write `termination_by?` to see the termination argument
inferred by GuessLex, and turn it into `termination_by …` using the “Try
this” widget or a code action.
@nomeata nomeata requested a review from Kha as a code owner February 27, 2024 11:01
@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 27, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6e408ee40259ad34afa1a8e8df8bece3a9029907 --onto c5fd88f5e118738425dd55b7592de435b7db8483. (2024-02-27 11:18:26)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 27, 2024 13:51 Inactive
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Feb 27, 2024
@leodemoura leodemoura added this pull request to the merge queue Feb 27, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 27, 2024
@leodemoura leodemoura added this pull request to the merge queue Feb 27, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Feb 27, 2024

This seems to be a bootstrapping issue, stage 2 doesn’t build.

@nomeata nomeata removed this pull request from the merge queue due to a manual request Feb 27, 2024
nomeata
nomeata commented Feb 27, 2024
View reviewed changes
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 27, 2024 22:31 Inactive
@nomeata nomeata enabled auto-merge February 28, 2024 09:03
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 28, 2024 10:31 Inactive
@nomeata nomeata added this pull request to the merge queue Feb 28, 2024
Merged via the queue into master with commit b9c4a7e Feb 28, 2024
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Awaiting requested review from Kha

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