leanprover
Paste result from Ctrl-P # to the Cursor
Right now, when using Ctrl-P # to find a theorem/lemma, the only options are to press Enter and open the file the lemma is in, or press Ctrl-Enter and open it to the side.
For short lemma names, it's possible to remember it and just type it again, but for longer ones, eg. div_le_div_of_mul_sub_mul_div_nonpos, it's harder to remember it. It would be nice if there was a keybinding that would just paste the highlighted lemma name to the cursor location.
It is possible to type in the beginning of the name of the lemma and then use Ctrl-Space, but having this would be a nice quality of life addition in my opinion.
Sadly, I don't think there's a way to do this with the same Ctrl-p # keybind, since that pulls up VS Code's symbol search menu and as far as I can tell we can't detect which menu item is highlighted from the extension.
It would be more work, but I think it would be possible to implement a separate custom menu that fetches the same list of declarations from the Lean server and then pastes the name at the cursor when it is selected.
