slice — Mathlib

Lean4
/-- `slice` is a conv tactic; if the current focus is a composition of several morphisms,
`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.
Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
-/
@[conv_parser 1000]
public meta def slice : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `slice 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "slice " false✝) (ParserDescr.const✝ `num))
        (ParserDescr.const✝ `ppSpace))
      (ParserDescr.const✝ `num))
Похожие утверждения