Skip to content

feat: allow disabling termination warnings when using addPreDefinitions - #14912

Open
Rob23oba wants to merge 2 commits into
leanprover:masterfrom
Rob23oba:nowarn-termination-option
Open

feat: allow disabling termination warnings when using addPreDefinitions#14912
Rob23oba wants to merge 2 commits into
leanprover:masterfrom
Rob23oba:nowarn-termination-option

Conversation

@Rob23oba

@Rob23oba Rob23oba commented Aug 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds an option to TerminationHints to disable warnings for redundant hints. This can be useful for generating declarations with termination hints using addPreDefinitions, avoiding warnings if these hints turn out to be redundant.

@github-actions github-actions Bot added the changelog-language Language features and metaprograms label Aug 24, 2026
@Rob23oba
Rob23oba marked this pull request as ready for review August 24, 2026 15:47
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Aug 24, 2026
@leanprover-bot

leanprover-bot commented Aug 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • 🟡 Reference manual branch lean-pr-testing-14912 build against this PR didn't complete normally. (2026-08-24 16:00:06) View Log
  • ✅ Reference manual branch lean-pr-testing-14912 has successfully built against this PR. (2026-08-24 16:03:31) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dd9cb93def1f4678434f84afb72ee8378c0800e4 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-24 16:21:38)

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Aug 24, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 24, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dd9cb93def1f4678434f84afb72ee8378c0800e4 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-24 16:21:37)
  • ✅ Mathlib branch lean-pr-testing-14912 has successfully built against this PR. (2026-08-24 16:48:07) View Log

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Aug 24, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@nomeata nomeata nomeata approved these changes

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

3 participants

@Rob23oba @leanprover-bot @nomeata