guess the import

Stream: lean4

[Kevin Buzzard]

In Lean 3 I really loved the fact that if I wanted to import continuous functions but I have no idea what the actual name of the import is, but I can remember that it involves continuity or continuous or something, then I can just type import continu, press ctrl-space, and see all the possible valid mathlib imports; from there it's really easy to spot that import topology.continuous_function.basic is what I want.

In Lean 4 I can't get this to work. I wanted to import whatsnew and I knew the import was Import something.something.whatsnew or something like that, maybe in Std or mathlib, but I am old and stupid and I can't remember exactly where it is or how to capitalise it, so I type import whatsnew and press ctrl-space and I get nothing. Is there another trick? I just have to switch to the searchbar and search all of mathlib for whatsnew and then switch back and type in whatever I found manually. Hardly the end of the world, but the Lean 3 version was cooler :-)

[Henrik Böving]

When we do regular programming in other languages quite often there is a code action that automatically searches through the available names from other files and suggests you to import this and that file. It'd be pretty cool if we could have a code action like that in the future.

[Wojciech Nawrocki]

Auto-completion for imports is not implemented yet but lean4#1884 made some headway towards it.

[Sebastian Ullrich]

Also, when what you're looking for is not a specific import but a declaration in some import, workspace symbol search (Ctrl-T) can show you the file name it's defined in