Documentation

Mathlib.Lean.GoalsLocation

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

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

The root expression of the position specified by the GoalsLocation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.SubExpr.GoalsLocation.pos :
    Lean.SubExpr.GoalsLocation → Lean.SubExpr.Pos

    The SubExpr.Pos specified by the GoalsLocation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.SubExpr.GoalsLocation.location :
      Lean.SubExpr.GoalsLocation → Lean.MetaM (Option Lean.Name)

      The hypothesis specified by the GoalsLocation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For