chore: switch the association of stored suggestions #11590
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
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 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.