sliceLHS — Mathlib

Lean4
/-- `slice_lhs a b => tac` zooms to the left-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 sliceLHS : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `sliceLHS 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "slice_lhs " false✝)
              (ParserDescr.const✝ `num))
            (ParserDescr.const✝ `ppSpace))
          (ParserDescr.const✝ `num))
        (ParserDescr.symbol✝ " => "))
      Lean.Parser.Tactic.Conv.convSeq)
Похожие утверждения