This PR fixes an issue where private definitions recursively invoked using generalized field notation (dot notation) would give an "invalid field" errors. It also fixes an issue where "invalid field notation" errors would pretty print the name of the declaration with a `_private` prefix. Closes #10044 |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||