# The `slice`

tactic #

Applies a tactic to an interval of terms from a term obtained by repeated application
of `Category.comp`

.

`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`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

- rewrites the target expression using
`Category.assoc`

. - uses
`congr`

to split off the first`a-1`

terms and rotates to`a`

-th (last) term - counts the number
`k`

of rewrites as it uses`←Category.assoc`

to bring the target to left associated form; from the first step this is the total number of remaining terms from`C`

- it now splits off
`b-a`

terms from target using`congr`

leaving the desired subterm - finally, it rewrites it once more using
`Category.assoc`

to bring it to right-associated normal form

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`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`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`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`

.

## Equations

- One or more equations did not get rendered due to their size.