[Agda] two expressions in the same hole?

[James Wood]

Hi Robby,

In this situation, I tend to use _,′_ from Data.Product. The idea is the 
same as you must have tried with _,_ , but the version with the prime 
gets rid of the possibility of dependency, allowing synthesis of the 
non-dependent product type in cases where both immediate subterms 
synthesise their types.

All the best,
James

On 31/05/2024 12:42, Robby Findler wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda