Closed
Description
The call to isFunction
fails on impredicative holes, resulting in the Introduce lambda
code action not appearing, and the intros
tactic making no progress. The ctxDefiningFuncs
has a corresponding polytype that we can use instead, but it's non-trivial to determine if we've already bound any arguments.