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: Dec 07 2023 at 09:01 UTC