mathlib documentation

tactic.chain

source
@[protected, 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_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.

source
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.

source
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.

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)