mathlib documentation

tactic.slice

meta def tactic.repeat_with_results {α : Type} :
tactic αtactic (list α)

meta def tactic.repeat_count {α : Type} :

meta def conv.repeat_with_results {α : Type} :
tactic αtactic (list α)

meta def conv.repeat_count {α : Type} :

meta def conv.slice  :
conv unit

meta def conv.slice_lhs  :
conv unittactic unit

meta def conv.slice_rhs  :
conv unittactic unit

meta def conv.interactive.slice  :
conv unit

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.