sliceRHS — Mathlib

Lean4
/-- `slice_rhs a b => tac` zooms to the right-hand side, uses associativity for categorical
composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
-/
@[tactic_parser 1000]
public meta def sliceRHS : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `sliceRHS 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "slice_rhs " false✝)
              (ParserDescr.const✝ `num))
            (ParserDescr.const✝ `ppSpace))
          (ParserDescr.const✝ `num))
        (ParserDescr.symbol✝ " => "))
      Lean.Parser.Tactic.Conv.convSeq)
Похожие утверждения