Proposal

Autocompletion of imports is currently missing in Lean 4, and is an important usability issue.

It is slightly difficult to implement, as when the imports are incomplete we likely can't even start the server, so it will require custom support in the VSCode extension.

Community Feedback

• https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Lean.20FRO/near/388986233
• https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean4.20autocomplete

I think this is already on @mhuisi's todo list, but I'm creating this issue to make sure there is a public tracker for it!

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.