4338a8be32
This PR fixes a bad error message due to elaborating partial syntax with Verso docstrings. When elaborating partial syntax, the elaborator sometimes attempts to add a docstring for a declaration that it didn't parse a name for. The name defaults to anonymous, but inserting the docs for the anonymous name throws a panic about being on the wrong async branch. With this change, the reported error is the expected parser error instead, which is much friendlier. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||