Lean4
/-- `conv in pat => cs` runs the `conv` tactic sequence `cs`
on the first subexpression matching the pattern `pat` in the target.
The converted expression becomes the new target subgoal, like `conv => cs`.
The arguments `in` are the same as those as the in `pattern`.
In fact, `conv in pat => cs` is a macro for `conv => pattern pat; cs`.
The syntax also supports the `occs` clause. Example:
```lean
conv in (occs := *) x + y => rw [add_comm]
```
-/
@[conv_parser 1000]
public meta def «convConvIn__=>_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Conv.«convConvIn__=>_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "conv" false✝) (ParserDescr.symbol✝ " in "))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.Conv.occs))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ " => "))
Lean.Parser.Tactic.Conv.convSeq)
