mathlib documentation

tactic.slice

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

source
meta def tactic.repeat_count {α : Type} (t : tactic α) :
tactic ℕ

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

source
meta def conv.repeat_count {α : Type} (t : tactic α) :
tactic ℕ

source
meta def conv.slice (a b : ℕ) :
conv unit

source
meta def conv.slice_lhs (a b : ℕ) (t : conv unit) :
tactic unit

source
meta def conv.slice_rhs (a b : ℕ) (t : conv unit) :
tactic unit

source
meta def conv.interactive.slice (a b : ℕ) :
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.

source
meta def tactic.interactive.slice_lhs (a b : interactive.parse lean.parser.small_nat) (t : conv.interactive.itactic) :
tactic unit

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.

source
meta def tactic.interactive.slice_rhs (a b : interactive.parse lean.parser.small_nat) (t : conv.interactive.itactic) :
tactic unit

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.