mathlib documentation

tactic.chain

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

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

meta def tactic.abstract_if_success {α : Type} :
(exprtactic α)exprtactic α

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

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

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