dd57725244
This PR introduces a new annotation that allows definitions to describe plausible-but-wrong name variants for the purpose of improving error messages. This PR just adds the notation and extra functionality; a stage0 update will allow standard Lean functions to have suggestion annotations. (Hence the changelog-no tag: this should go in the changelog when some preliminary annotations are actually added.) ## Example ```lean4 inductive MyBool where | tt | ff attribute [suggest_for MyBool.true] MyBool.tt attribute [suggest_for MyBool.false] MyBool.ff @[suggest_for MyBool.not] def MyBool.swap : MyBool → MyBool | tt => ff | ff => tt /-- error: Unknown constant `MyBool.true` Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`: M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲ -/ #guard_msgs in example := MyBool.true /-- error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression MyBool.tt of type `MyBool` Hint: Perhaps you meant one of these in place of `MyBool.not`: [apply] `MyBool.swap`: MyBool.tt.swap -/ #guard_msgs in example := MyBool.tt.not ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||