Commit 2021-08-18 18:52 e6fda2ac

fix(transform_decl): fix namespace bug (#8733)

• The problem was that when writing @[to_additive] def foo ... every declaration used in foo in namespace foo would be additivized without changing the last part of the name. This behavior was intended to translate automatically generated declarations like foo._proof_1. However, if foo contains a non-internal declaration foo.bar and add_foo.bar didn't exist yet, it would also create a declaration add_foo.bar additivizing foo.bar.
• This PR changes the behavior: if foo.bar has the @[to_additive] attribute (potentially with a custom additive name), then we won't create a second additive version of foo.bar, and succeed normally. However, if foo.bar doesn't have the @[to_additive] attribute, then we fail with a nice error message. We could potentially support this behavior, but it doesn't seem that worthwhile and it would require changing a couple low-level definitions that @[to_additive] uses (e.g. by replacing name.map_prefix so that it only maps prefixes if the name is internal).
• So far this didn't happen in the library yet. There are currently 5 non-internal declarations foo.bar that are used in foo where foo has the @[to_additive] attribute, but all of these declarations were already had an additive version add_foo.bar.
• These 5 declarations are [Mon.has_limits.limit_cone, Mon.has_limits.limit_cone_is_limit, con_gen.rel, magma.free_semigroup.r, localization.r]
• This fixes the error in #8707 and resolves the Zulip thread https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238707.20linter.20weirdness
• I also added some documentation / comments to the function transform_decl_with_prefix_fun_aux, made it non-private, and rewrote some steps.