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 firsta-1
terms and rotates toa
-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 fromC
- it now splits off
b-a
terms from target usingcongr
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
.