Documentation

Mathlib.Tactic.Recover

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.

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
    Instances For

      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
        Instances For