-
Joachim Breitner authored
when matching a lambda in the template against an expression. When matching, look through coercions (only for value lambdas for now), and look through currently active unfoldings, if these are undersaturated, i.e. produce a lambda. This replaces the existing, somewhat fishy eta-expansion.
a27b2985