suggest imports

Stream: lean4

[Kevin Buzzard]

Am I living in a dream world if I am hoping that, within mathlib, if I type example : IsTensorProduct then a little paperclip pops up saying "I see that you're looking for a declaration you've not imported: shall I add import Mathlib.RingTheory.IsTensorProduct at the top of your file?"?

[Eric Wieser]

This is probably a little fiddly as you'd want it to respect currently open namespace etc, but feels like something that could be supported by reading (possibly-out-of-date) ilean files

[Marc Huisinga]

Investigating this is on my to-do list.

[Arthur Paulino]

Kevin Buzzard said:

within mathlib

Ideally it would also check for dependencies, so not only within mathlib but also, for example, in a project that depends on mathlib

[Mario Carneiro]

The interface for this I like is the one from rust-analyzer, where autocomplete will suggest definitions which are not imported, with a (import Mathlib.Foo) line in the completion, and accepting the completion will both complete the identifier and also insert the import Mathlib.Foo line at the top of the file