Defines the swap_var tactic #

Swap the names of two hypotheses.

The parser for swap rules

Instances For

    swap_var swap_rule₁, swap_rule₂, ⋯ applies swap_rule₁ then swap_rule₂ then .

    A swap_rule is of the form x y or x ↔ y, and "applying it" means swapping the variable name x by y and vice-versa on all hypotheses and the goal.

    example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
      swap_var p ↔ q
      exact ⟨p, q⟩
    Instances For