mathlib documentation

tactic.slice

meta def tactic.repeat_with_results {α : Type} (t : tactic α) :
meta def tactic.repeat_count {α : Type} (t : tactic α) :
meta def conv.repeat_with_results {α : Type} (t : tactic α) :
meta def conv.repeat_count {α : Type} (t : tactic α) :
meta def conv.slice (a b : ) :
meta def conv.slice_lhs (a b : ) (t : conv unit) :
meta def conv.slice_rhs (a b : ) (t : conv unit) :
meta def conv.interactive.slice (a b : ) :

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.

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.

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.