Module Kernel.MatchingSource

solve_miller var t Solves the matching problem X x1 ... xn = t where var represents the applied Miller variable X x1 ... xn. Raises NotUnifiable in case there is no solution.

This is the default implementation. * It relies on the provided : * - whnf reduction strategy to flatten AC terms without digging to deep inside * - snf reduction strategy to perform higher order matching when necessary * - are_convertible convertibility test