search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
278 stars 27 forks source link

Action to accept lean's suggestion #347

Closed yakimk closed 3 months ago

yakimk commented 3 months ago

Didn't find anything concerning accepting lean's suggestions (I mean those popups after exact? or rw? for instance) . Would be quite handy to bind a shortcut for accepting first suggestion, since clicking on a popup doesn't insert it in place like in vscode and you have to copy it manually. Is there any kind of similar functionality that I missed?

Julian commented 3 months ago

Hey there!

These are called "code actions" -- and they're not specific to Lean, which is why lean.nvim doesn't really handle anything related to them, you just use "normal" neovim ways to activate these.

But, even more specifically -- my intention is to cover this and many other "non-Lean-related" topics in a new in-progress Manual -- so I just added the linked section there which should tell you what to touch to get these working.

Can you have a look and let me know if that's specific enough to answer the question here?

yakimk commented 3 months ago

Thank you! Exactly what I was looking for.