3bd1dd633f
This PR causes Lean to search through `@[suggest_for]` annotations on certain errors that look like unknown identifiers that got incorrectly autobound. This will correctly identify that a declaration of type `Maybe String` should be `Option String` instead. ## Example ``` example : Except String Unit := return .ok () ``` ``` Function expected at Result but this term has type ?m.1 Note: Expected a function because this term is being applied to the argument String Hint: The identifier `Result` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement. Perhaps you meant `Except` in place of `Result`? ``` The last line is added by this PR. |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||