# The `slice`

tactic #

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

.

- 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

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

.

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

.