mathlib documentation

tactic.transfer

source
@[instance]
meta def transfer.has_to_tactic_format_rel_data  :
has_to_tactic_format rel_data

source
@[instance]
meta def transfer.has_to_tactic_format_rule_data  :
has_to_tactic_format rule_data

source
meta def transfer.analyse_decls (a : list name) :
tactic (list rule_data)

source
meta def transfer.compute_transfer (a : list rule_data) (a_1 : list expr) (a_2 : expr) :
tactic (expr × expr × list expr)

source
meta def tactic.transfer (ds : list name) :
tactic unit