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.

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

      The SubExpr.Pos specified by the GoalsLocation.

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

          The hypothesis specified by the GoalsLocation.

          Equations
            Instances For