tacticNth_grw_____ — Mathlib

Lean4
/-- `nth_grw` is just like `nth_rw`, but for `grw`. -/
@[tactic_parser 1000]
public meta def tacticNth_grw_____ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.tacticNth_grw_____ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "nth_grw" 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))
Похожие утверждения