Lean4
/-- The tactic `introv` allows the user to automatically introduce the variables of a theorem and
explicitly name the non-dependent hypotheses.
Any dependent hypotheses are assigned their default names.
Examples:
```
example : ∀ a b : Nat, a = b → b = a := by
introv h,
exact h.symm
```
The state after `introv h` is
```
a b : ℕ,
h : a = b
⊢ b = a
```
```
example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
introv h₁ h₂,
exact h₁.trans h₂
```
The state after `introv h₁ h₂` is
```
a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c
```
-/
@[tactic_parser 1000]
public meta def introv : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.introv 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "introv " false✝)
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt)) Lean.binderIdent)))
