Zulip Chat Archive

Stream: general

Topic: Hole command for implicit args


Yakov Pechersky (Jun 23 2020 at 22:51):

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 (Jun 23 2020 at 23:04):

i think you want refine

Yakov Pechersky (Jun 23 2020 at 23:09):

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 (Jun 23 2020 at 23:11):

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 (Jun 23 2020 at 23:11):

I think this might actually exist already?


Last updated: Dec 20 2023 at 11:08 UTC