Stream: Coq devs & plugin devs

Topic: Decomposing syntactic patterns

view this post on Zulip Janno (Mar 16 2021 at 11:40):

I am dipping my toes into Constr_matching and I was wondering about the following: if I have a pattern f pat1 pat2 and a term f term1 term2, can I decompose the matching problem into term1 ~ pat1 and term2 ~ pat2 plus some kind of compatibility check on the two resulting variable assignments? If so, what would that check look like? In particular, would it be enough to check that their overlap is syntactically equal?

Last updated: Oct 15 2021 at 20:02 UTC