Documentation

Mathlib.Lean.GoalsLocation

This file defines some functions for dealing with SubExpr.GoalsLocation.

source
def Lean.SubExpr.GoalsLocation.rootExpr :
GoalsLocation → MetaM Expr

The root expression of the position specified by the GoalsLocation.

Instances For
    source
    def Lean.SubExpr.GoalsLocation.pos :
    GoalsLocation → Pos

    The SubExpr.Pos specified by the GoalsLocation.

    Instances For
      source
      def Lean.SubExpr.GoalsLocation.fvarId? :
      GoalsLocation → Option FVarId

      The hypothesis specified by the GoalsLocation.

      Instances For