vscode refactoring

Stream: general

[Matthew Pocock]

I may be missing it, but in the vscode plugin, my normal muscle-memory for the rename refactor isn't working. For example, renaming local variables. User error?

[Julian Berman]

Your normal muscle-memory I assume involves some code action present in another language you use?

If so, such a code action isn't yet written for Lean though it was discussed in another thread recently (which I can try to find).

[Julian Berman]

Oh, as usual, Mario has already managed to code it up... The PR (which is still open) is https://github.com/leanprover/lean4/pull/2462