vscode-lean4 RFC: “Inline variable” code action

Stream: lean4

[suhr]

“Inline variable” code action is an action which substitutes definition body in every expression where the definition is used. It is very useful in general but even more so in proofs.

I miss it every time when I use by exact? and by apply? to construct a proof.