[Agda] two expressions in the same hole?

[Robby Findler]

Hi all:

   I find myself sometimes wanting to work on two expressions in a single
hole at the same time. Typically one is going to be in an argument to the
other but they have to fit together in a certain way that I find hard to
predict without working through the details of each separately. Is there
some facility for doing that or some trick that folks use in similar
situations? I tried just separating them with a comma which works sometimes
but not always (when the pair constructor is in scope) as the dependency
sometimes gets in the way.

One example of this is `trans` -- when you're working on an equality proof
and you want to tweak both of them to get the thing that'll eventually end
up in the middle. (With trans specifically, actually, I've gotten used to
it enough that I don't actually need the help anymore, but hopefully it
makes the request clearer.)

tia,
Robby
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20240531/211ea342/attachment.html>