Lean4
/-- `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.
```lean
example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
swap_var p ↔ q
exact ⟨p, q⟩
```
-/
@[tactic_parser 1000]
public meta def «tacticSwap_var__,,» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.«tacticSwap_var__,,» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "swap_var " false✝)
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝)
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) Mathlib.Tactic.swapRule) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))
