Documentation

Std.Tactic.SeqFocus

Assuming there are n goals, map_tacs [t1; t2; ...; tn] applies each ti to the respective goal and leaves the resulting subgoals.

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

    t <;> [t1; t2; ...; tn] focuses on the first goal and applies t, which should result in n subgoals. It then applies each ti to the corresponding goal and collects the resulting subgoals.

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