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 12 2024 at 11:01 UTC