08c87b2ad3
This PR gives a focused error message when a user tries to name an example, and tweaks error messages for attempts to define multiple opaque names at once. ## Example errors ``` example x : 1 == 1 := by grind ``` Current message: ``` Failed to infer type of binder `x` Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be ``` New message: ``` Failed to infer type of binder `x` Note: Examples don't have names. The identifier `x` is being interpreted as a parameter `(x : _)`. ``` ## Plural-aware identifier lists Both the example errors and opaque errors understand pluralization and use oxford commas. ``` opaque a b c : Nat ``` Current message: ``` Failed to infer type of binder `c` Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`. ``` New message: ``` Failed to infer type of binder `c` Note: Multiple constants cannot be declared in a single declaration. The identifiers `b` and `c` are being interpreted as parameters `(b : _)` and `(c : _)`.``` |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||