Zulip Chat Archive

Stream: general

Topic: implicit conv congr

Patrick Massot (Oct 06 2018 at 16:43):

In conv mode, is there a version of congr/skip which allow traverse implicit arguments?

Patrick Massot (Oct 07 2018 at 21:25):

@Mario Carneiro did you see this question?

Mario Carneiro (Oct 08 2018 at 00:32):

I don't think congr decides things based on whether they are implicit, but rather whether they are dependent on other arguments

Patrick Massot (Oct 08 2018 at 09:04):

I made a few tests, and it seems you're right. So my new question is: how to you conv or rw dependent arguments? I guess this is the same issue I have when I want to use assumptions stating that two uniform structures are the same

Last updated: Aug 03 2023 at 10:10 UTC