Extended Abstract: From Pattern Unification Towards Pattern Matching Unification

David Richter, Timon Böhler

We revisit the role of higher-order unification in dependently typed languages and identify a fundamental limitation of existing pattern-based fragments: their inability to synthes…