Hole command for implicit args

Stream: general

[Yakov Pechersky]

A cool hole command would be when doing

rw @complicated_func _

the hole command would expand the underscore to as many underscores as there are implicit and explicit arguments to complicated_func

[Jalex Stark]

i think you want refine

[Yakov Pechersky]

Sure! But that splits it into goals. When there are many arguments that can be inferred other than that 1 single tricky one, I picture refine leading to a lot of sorry or swap to get to the one tricky one, then undoing the refine back into a rw @complicated _ _ _ _ myarg _ _. Is that what you mean?

[Jalex Stark]

i see, your point is just that you may end up typing all of the underscores anyway, and you'd like automation for this

[Reid Barton]

I think this might actually exist already?