Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Improve `:Telescope loogle` #317

Open hargoniX opened 9 months ago

hargoniX commented 9 months ago

As discussed in #316 we would like a few improvements:

Julian commented 9 months ago

Another different path to think about I think is integrating with the workspace -- e..g maybe it'd be nice to have a Loogle searcher where it helps you assemble your query using current LSP workspace symbols.

(I'm purely dreaming up crude ideas here) but just like e.g. require('telescope.builtin').lsp_dynamic_workspace_symbols() will telescope over all the Lean stuff you're currently importing, perhaps it'd be nice to combine that with Loogle such that you could type a query like Re. ?a Re. and have telescope help you convert the Re to Real.sin (because you've imported that).

Obviously that starts to use some more complicated telescope functionality but I think something like that should be feasible (of course not saying it's urgent, but I like that we can collect ideas).