9e87560376
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. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Basic2.lean | ||
| ConflictingImported.lean | ||
| Imported.lean | ||
| ImportedAll.lean | ||
| ImportedAllImportedAll.lean | ||
| ImportedAllPrivateImported.lean | ||
| ImportedImportedAll.lean | ||
| ImportedPrivateImported.lean | ||
| MetaImported.lean | ||
| NonModule.lean | ||
| PrivateImported.lean | ||