Reduced the issue to a self-contained, reproducible test case.
Description
Since Lean syntax is extensible, there is no easy way to write it down or discover what is valid at any point in a Lean program. Therefore I propose we add a syntax element to the LSP for completion prompts. We could use different icons to represent "syntax" from "members".
Steps to Reproduce
Expected behavior:
show the user that the keyword "where" is allowed here.
Actual behavior:
it only shows 'members' of current namespaces...
Reproduces how often:
The problem is where is not documented in the theorem proving book, and our reference docs are very incomplete, so there is now way to know the where clause is valid here unless you go an read all the Lean compiler source code and new users shouldn't have to do that.
Prerequisites
Description
Since Lean syntax is extensible, there is no easy way to write it down or discover what is valid at any point in a Lean program. Therefore I propose we add a syntax element to the LSP for completion prompts. We could use different icons to represent "syntax" from "members".
Steps to Reproduce
Expected behavior:
show the user that the keyword "where" is allowed here.
Actual behavior:
it only shows 'members' of current namespaces...
Reproduces how often:
The problem is
where
is not documented in the theorem proving book, and our reference docs are very incomplete, so there is now way to know thewhere
clause is valid here unless you go an read all the Lean compiler source code and new users shouldn't have to do that.Versions
Lean (version 4.0.0-nightly-2021-12-13, commit 3a6cc774241b, Release)
Additional Information
Any additional information, configuration or data that might be necessary to reproduce the issue.