ink

def Mathlib.Tactic.getUnassignedGoalMVarDependencies (mvarId : Lean.MVarId) : Lean.MetaM (Lean.HashSet Lean.MVarId)

Get all metavariables which mvarId depends on. These are the metavariables which occur in the target or local context or delayed assignment (if any) of mvarId, plus the metvariables which occur in these metavariables, etc.

Equations

• Mathlib.Tactic.getUnassignedGoalMVarDependencies mvarId = do let __do_lift ← StateRefT'.run (Mathlib.Tactic.getUnassignedGoalMVarDependencies.go mvarId) ∅ pure __do_lift.snd

ink

partial def Mathlib.Tactic.getUnassignedGoalMVarDependencies.addMVars (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

auxiliary function for getUnassignedGoalMVarDependencies

ink

partial def Mathlib.Tactic.getUnassignedGoalMVarDependencies.go (mvarId : Lean.MVarId) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

auxiliary function for getUnassignedGoalMVarDependencies

ink

def Mathlib.Tactic.tacticRecover_ : Lean.ParserDescr

Modifier recover for a tactic (sequence) to debug cases where goals are closed incorrectly. The tactic recover tacs for a tactic (sequence) tacs applies the tactics and then adds goals that are not closed starting from the original

Equations

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