convRHS — Mathlib

Lean4
@[tactic_parser 1000]
public meta def convRHS : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Conv.convRHS 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "conv_rhs" false✝)
            (ParserDescr.unary✝ `optional
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " at ") (ParserDescr.const✝ `ident))))
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " in ")
                (ParserDescr.unary✝ `optional Lean.Parser.Tactic.Conv.occs))
              (ParserDescr.cat✝ `term 0))))
        (ParserDescr.symbol✝ " => "))
      Lean.Parser.Tactic.Conv.convSeq)
Похожие утверждения