mathlib documentation

tactic.​transform_decl

tactic.​transform_decl

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

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