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 = fvarId.getType
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }.rootExpr = fvarId.getType
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }.rootExpr = do let __do_lift ← fvarId.getDecl pure __do_lift.value
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }.rootExpr = mvarId.getType

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.location : GoalsLocation → MetaM (Option Name)

The hypothesis specified by the GoalsLocation.

Equations

• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hyp fvarId }.location = some <$> fvarId.getUserName
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }.location = some <$> fvarId.getUserName
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }.location = some <$> fvarId.getUserName
• { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }.location = pure none