feat: generalize withSetOptionIn to arbitrary result types - #14581
Merged
wkrozowski merged 1 commit intoJul 29, 2026
Conversation
marcelolynch
marked this pull request as ready for review
July 28, 2026 14:11
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Draft
1 task
wkrozowski
force-pushed
the
generalize-withSetOptionIn
branch
from
July 29, 2026 13:01
907fc08 to
b06524b
Compare
wkrozowski
requested review from
TwoFX,
kim-em,
kmill,
leodemoura and
sgraf812
as code owners
July 29, 2026 13:01
wkrozowski
force-pushed
the
generalize-withSetOptionIn
branch
from
July 29, 2026 13:02
b06524b to
907fc08
Compare
The phases of a stateful linter (leanprover#14357) return values, so they cannot use the CommandElab-only signature. All existing call sites instantiate the result type with Unit and do not change. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
wkrozowski
force-pushed
the
generalize-withSetOptionIn
branch
from
July 29, 2026 13:02
907fc08 to
47b10a0
Compare
github-actions
Bot
added
the
mathlib4-nightly-available
leanprover-bot
added
the
builds-manual
Contributor
|
LGTM |
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
robsimmons
pushed a commit
that referenced
this pull request
Jul 29, 2026
This PR generalizes `withSetOptionIn` over the result type of the wrapped function. The previous signature only accepted a `CommandElab`, which returns `Unit`. The phases of a stateful linter (#14357) return values, so they could not use the helper (see for example leanprover-community/mathlib4#42186). All existing call sites instantiate the result type with `Unit` and do not change. A new `resultType` section in `tests/elab/withSetOptionIn.lean` checks the generalized signature. The change preserves behavior. Type inference changes in one corner case: a first-class use with no expected type, where the wrapped function does not determine its result type, now needs a type ascription. Core, Batteries, and Mathlib contain no such use. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR generalizes
withSetOptionInover the result type of the wrapped function. The previous signature only accepted aCommandElab, which returnsUnit. The phases of a stateful linter (#14357) return values, so they could not use the helper (see for example leanprover-community/mathlib4#42186). All existing call sites instantiate the result type withUnitand do not change.A new
resultTypesection intests/elab/withSetOptionIn.leanchecks the generalized signature.The change preserves behavior. Type inference changes in one corner case: a first-class use with no expected type, where the wrapped function does not determine its result type, now needs a type ascription. Core, Batteries, and Mathlib contain no such use.
🤖 Generated with Claude Code