mathlib docs: tactic.transform

meta def tactic.transform_decl_with_prefix_fun (f : name → option name) (src tgt : name) (attrs : list name) :

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the function f. This is used to implement @[to_additive].

source

meta def tactic.transform_decl_with_prefix_dict (dict : name_map name) (src tgt : name) (attrs : list name) :

tactic unit

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the dictionary dict. This is used to implement @[to_additive].