mathlib3 documentation

tactic.chain

@[protected, instance]
meta def tactic.tactic_script_unit_has_to_string  :
has_to_string (tactic.tactic_script unit)
meta def tactic.abstract_if_success {α : Type} (tac : expr tactic α) (g : expr) :
meta def tactic.chain_single {α : Type} (tac : tactic α) :
expr tactic × list (tactic.tactic_script α))

chain_many tac recursively tries tac on all goals, working depth-first on generated subgoals, until it no longer succeeds on any goal. chain_many automatically makes auxiliary definitions.

meta def tactic.chain_iter {α : Type} (tac : tactic α) :
list expr list expr tactic (list (tactic.tactic_script α))

chain_many tac recursively tries tac on all goals, working depth-first on generated subgoals, until it no longer succeeds on any goal. chain_many automatically makes auxiliary definitions.

meta def tactic.chain_many {α : Type} (tac : tactic α) :
list expr tactic (list (tactic.tactic_script α))

chain_many tac recursively tries tac on all goals, working depth-first on generated subgoals, until it no longer succeeds on any goal. chain_many automatically makes auxiliary definitions.

meta def tactic.chain_core {α : Type} [has_to_string (tactic.tactic_script α)] (tactics : list (tactic α)) :
meta def tactic.trace_output {α : Type} [has_to_string (tactic.tactic_script α)] [has_to_format α] (t : tactic α) :
meta def tactic.chain {α : Type} [has_to_string (tactic.tactic_script α)] [has_to_format α] (tactics : list (tactic α)) :