Closed
Description
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.