feat: @[suggest_for] attribute to inform replacements
#11367
Merged
Conversation
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
robsimmons
force-pushed
the
suggest-replacements
branch
2 times, most recently
from
8784f32 to
b164835
Compare
robsimmons
force-pushed
the
suggest-replacements
branch
from
59d96f9 to
33076bc
Compare
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
github-merge-queue bot
pushed a commit
that referenced
this pull request
Dec 5, 2025
This PR fixes a syntax-pattern-matching issue from #11367 that prevented the addition of suggestions in Init prior to Lean.Parser being introduced, which was a significant shortcoming. It preserves the ability to have multiple suggestions for one annotation later in the process. Additionally, tweaks a (not-yet-user-visible) error message and modifies the attribute declaration to store a wrongIdentifier -> correctIdentifier mapping instead of a correctIdentifier -> wrongIdentifier mapping.
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
This PR introduces a new annotation that allows definitions to describe plausible-but-wrong name variants for the purpose of improving error messages. This PR just adds the notation and extra functionality; a stage0 update will allow standard Lean functions to have suggestion annotations. (Hence the changelog-no tag: this should go in the changelog when some preliminary annotations are actually added.) ## Example ```lean4 inductive MyBool where | tt | ff attribute [suggest_for MyBool.true] MyBool.tt attribute [suggest_for MyBool.false] MyBool.ff @[suggest_for MyBool.not] def MyBool.swap : MyBool → MyBool | tt => ff | ff => tt /-- error: Unknown constant `MyBool.true` Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`: M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲ -/ #guard_msgs in example := MyBool.true /-- error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression MyBool.tt of type `MyBool` Hint: Perhaps you meant one of these in place of `MyBool.not`: [apply] `MyBool.swap`: MyBool.tt.swap -/ #guard_msgs in example := MyBool.tt.not ```
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
This PR fixes a syntax-pattern-matching issue from #11367 that prevented the addition of suggestions in Init prior to Lean.Parser being introduced, which was a significant shortcoming. It preserves the ability to have multiple suggestions for one annotation later in the process. Additionally, tweaks a (not-yet-user-visible) error message and modifies the attribute declaration to store a wrongIdentifier -> correctIdentifier mapping instead of a correctIdentifier -> wrongIdentifier mapping.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Dec 10, 2025
This PR switches the way olean files store identifier suggestions. The ordering introduced in #11367 and #11529 made sense if we were only storing incorrect -> correct mappings, but for the reference manual we want to store the correct -> incorrect mappings as well, and so it is more sensible to store just the correct -> incorrect mapping that mimics the author-generated data better. Also tweaks error messages further in preparation for public-facing @[suggest_for] annotations and forbids suggestions on non-public names. Does not make generally-visible changes as there are no introduced uses of @[suggest_for] annotations yet.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Dec 10, 2025
…11554) This PR adds `@[suggest_for]` annotations to Lean, allowing lean to provide corrections for `.every` or `.some` methods in place of `.all` or `.any` methods for most default-imported types (arrays, lists, strings, substrings, and subarrays, and vectors). Due to the need for stage0 updates for new annotations, the `suggest_for` annotation itself was introduced in previous PRs: #11367, #11529, and #11590. ## Example ``` example := "abc".every (! ·.isWhitespace) ``` Error message: ``` Invalid field `every`: The environment does not contain `String.every`, so it is not possible to project the field `every` from an expression "abc" of type `String` Hint: Perhaps you meant `String.all` in place of `String.every`: .e̵v̵e̵r̵y̵a̲l̲l̲ ``` (the hint is added by this PR) ## Additional changes Adds suggestions that are not currently active but that can be used to generate autocompletion suggestions in the reference manual: - `Either` -> `Except` and `Sum` - `Exception` -> `Except` - `ℕ` -> `Nat` - `Nullable` -> `Option` - `Maybe` -> `Option` - `Optional` -> `Option` - `Result` -> `Except`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 introduces a new annotation that allows definitions to describe plausible-but-wrong name variants for the purpose of improving error messages.
This PR just adds the notation and extra functionality; a stage0 update will allow standard Lean functions to have suggestion annotations. (Hence the changelog-no tag: this should go in the changelog when some preliminary annotations are actually added.)
Example