# The `recover` tactic modifier #

This defines the `recover` tactic modifier, which can be used to debug cases where goals are not closed correctly. `recover tacs` for a tactic (or tactic sequence) `tacs` applies the tactics and then adds goals that are not closed, starting from the original goal.

source
def Mathlib.Tactic.getUnassignedGoalMVarDependencies (mvarId : Lean.MVarId) :
Lean.MetaM (Std.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 metavariables which occur in these metavariables, etc.

Equations

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

Instances For

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

auxiliary function for `getUnassignedGoalMVarDependencies`

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

auxiliary function for `getUnassignedGoalMVarDependencies`

source
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 goal.

Equations

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

Instances For