@leanprover/infoview
    Preparing search index...

    Type Alias GoalLocation

    GoalLocation:
        | { hyp: FVarId }
        | { hypType: [FVarId, SubexprPos] }
        | { hypValue: [FVarId, SubexprPos] }
        | { target: SubexprPos }

    A location within a goal. It is either:

    • one of the hypotheses; or
    • (a subexpression of) the type of one of the hypotheses; or
    • (a subexpression of) the value of one of the let-bound hypotheses; or
    • (a subexpression of) the goal type.

    Settings
    Member Visibility