[isabelle] Higher-order matching and unification


I see that higher-order pattern matching is a decidable fragment of
higher-order unification. With matching, one of the expressions must be
closed. So does that mean HO pattern matching is essentially a flex-rigid
problem? If so, does that mean unifying a flex-rigid pair is guaranteed to
be decidable?

Thank you for your time.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.