Use exprIsLambda_maybe in match
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.
Please register or sign in to comment