tacticNth_grewrite_____ — Mathlib

Lean4
/-- `nth_grewrite` is just like `nth_rewrite`, but for `grewrite`. -/
@[tactic_parser 1000]
public meta def tacticNth_grewrite_____ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.tacticNth_grewrite_____ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "nth_grewrite" false✝)
              Lean.Parser.Tactic.optConfig)
            (ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
          (ParserDescr.unary✝ `many1 (ParserDescr.const✝ `num)))
        Lean.Parser.Tactic.rwRuleSeq)
      (ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
Похожие утверждения