copy_attribute' attr_name src tgt p d_name copy (user) attribute attr_name from
src to tgt if it is defined for src; unlike copy_attribute the primed version also copies
the parameter of the user attribute, in the user attribute case. Make it persistent if p is
tt; if p is none, the copied attribute is made persistent iff it is persistent on src
additive_test f replace_all ignore e tests whether the expression e contains no constant
nm that is not applied to any arguments, and such that f nm = none.
This is used in @[to_additive] for deciding which subexpressions to transform: we only transform
constants if additive_test applied to their first argument returns tt.
This means we will replace expression applied to e.g. α or α × β, but not when applied to
e.g. ℕ or ℝ × α.
f is the dictionary of declarations that are in the to_additive dictionary.
We ignore all arguments specified in the name_mapignore.
If replace_all is tt the test always return tt.
transform the declaration src and all declarations pre._proof_i occurring in src
using the dictionary f.
replace_all, trace, ignore and reorder are configuration options.
pre is the declaration that got the @[to_additive] attribute and tgt_pre is the target of this