Suggestion for VSCode: Imports

Stream: lean4

[Shreyas Srinivas]

This is more of a suggestion than an issue to be fixed. Normally when I start working on a file I start with import Mathlib which comes in handy because I might not remember exactly which mathlib files I need to import. At the same time, when I share the code with others, depending on how cache works for them, they might prefer it if only the relevant files were imported. When I write haskell or rust, the vscode extension automatically adds and fixes my imports as I use names in my file. Is such a feature feasible for the vscode extension for lean?

[Alex Keizer]

It definetely seems feasible. I expect the biggest reason it doesn't exist yet is just that it's quite a lot of engineering effort to make it work, and it hasn't been a priority so far.