Lsp code actions that will insert a `rw?` result?

Stream: general

[nrs]

I'm using lean.nvim, and I'm trying to make the workflow of using rw?, simp?, apply? a bit faster; are there code actions that will insert a lemma from the infoview at the cursor location?

[Julian Berman]

Yes, all the above produce such a code action.

[nrs]

Julian Berman said:

Yes, all the above produce such a code action.

ah fantastic thank you, have been using lean.nvim for two months and it seems have preferred to suffer copy/pasting with my mouse instead of reading the docs (also thanks a lot for the work on lean.nvim!!!)

[Patrick Massot]

Note we are still missing the corresponding widgets showing the remaining goals.