mathlib3 documentation

tactic.transfer

source
@[protected, instance]
meta def transfer.has_to_tactic_format_rel_data  :
has_to_tactic_format rel_data
source
@[protected, instance]
meta def transfer.has_to_tactic_format_rule_data  :
has_to_tactic_format rule_data
source
meta def transfer.analyse_decls  :
list name → tactic (list rule_data)
source
meta def transfer.compute_transfer  :
list rule_data → list expr → expr → tactic (expr × expr × list expr)
source
meta def tactic.transfer (ds : list name) :
tactic unit