Zulip Chat Archive

Stream: general

Topic: implicit conv congr


view this post on Zulip Patrick Massot (Oct 06 2018 at 16:43):

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

view this post on Zulip Patrick Massot (Oct 07 2018 at 21:25):

@Mario Carneiro did you see this question?

view this post on Zulip 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

view this post on Zulip 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: May 09 2021 at 19:11 UTC