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.

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

def Mathlib.Tactic.tacticRecover_ : Lean.ParserDescr

recover tacs applies the tactic (sequence) tacs and then re-adds goals that were incorrectly marked as closed. This helps to debug issues where a tactic closes goals without solving them (i.e. goals were removed from the MetaM state without the metavariable being assigned), resulting in the error "(kernel) declaration has metavariables".

Equations

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