[Feature request/question] Record completion as a (lens) code action

[googleson78]

Would it be possible and/or desired to also get this functionality as a code action/code lens action?

I don't use snippets/autocomplete, and would prefer to use it via those interfaces.

There's also another option, used in Agda, where attempting to "introduce constructor" (refine goal) for a hole automatically generates all the field with holes left for each one.

[isovector]

Fixed by #1356 and ##1461