mathlib documentation

tactic.chain

source
@[instance]
meta def tactic.has_to_string  :
has_to_string (tactic.tactic_script string)

source
@[instance]
meta def tactic.tactic_script_unit_has_to_string  :
has_to_string (tactic.tactic_script unit)

source
meta def tactic.abstract_if_success {α : Type} (tac : expr → tactic α) (g : expr) :
tactic α

source
meta def tactic.chain_core {α : Type} [has_to_string (tactic.tactic_script α)] (tactics : list (tactic α)) :
tactic (list string)

source
meta def tactic.trace_output {α : Type} [has_to_string (tactic.tactic_script α)] [has_to_format α] (t : tactic α) :
tactic α

source
meta def tactic.chain {α : Type} [has_to_string (tactic.tactic_script α)] [has_to_format α] (tactics : list (tactic α)) :
tactic (list string)