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

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

The root expression of the position specified by the GoalsLocation.

Equations

• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hyp fvarId }.rootExpr = do let __do_lift ← fvarId.getType Lean.instantiateMVars __do_lift
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }.rootExpr = do let __do_lift ← fvarId.getType Lean.instantiateMVars __do_lift
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }.rootExpr = do let __do_lift ← fvarId.getDecl Lean.instantiateMVars __do_lift.value
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }.rootExpr = do let __do_lift ← mvarId.getType Lean.instantiateMVars __do_lift

def Lean.SubExpr.GoalsLocation.pos : GoalsLocation → Pos

The SubExpr.Pos specified by the GoalsLocation.

Equations

• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hyp fvarId }.pos = Lean.SubExpr.Pos.root
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }.pos = a
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }.pos = a
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }.pos = a

def Lean.SubExpr.GoalsLocation.fvarId? : GoalsLocation → Option FVarId

The hypothesis specified by the GoalsLocation.

Equations

• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hyp fvarId }.fvarId? = some fvarId
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }.fvarId? = some fvarId
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }.fvarId? = some fvarId
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }.fvarId? = none