Skip to content

Wingman can't run "introduce lambda" on impredicative holes #1571

Closed
@isovector

Description

@isovector

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.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions