Topic: implicit conv congr
Patrick Massot (Oct 06 2018 at 16:43):
In conv mode, is there a version of
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: May 09 2021 at 19:11 UTC