Commit 2022-05-04 17:58 abcd601c

fix(src/tactic/alias): Teach get_alias_target about alias f ↔ a b (#13742) the get_alias_target function in alias.lean is used by the to_additive command to add the “Alias of …” docstring when creating an additive version of an existing alias (this was #13330). But get_alias_target did not work for alias f ↔ a b. This fixes it by extending the alias_attr map to not just store whether a defintion is an alias, but also what it is an alias of. Much more principled than trying to reconstruct the alias target from the RHS of the alias definition. Note that alias currently says “Alias of foo_iff” even though it’s really an alias of foo_iff.mp. This is an existing bug, not fixed in this PR – the effect is just that this “bug” will uniformly apply to additive lemmas as well. Hopefully will get rid of plenty of nolint.txt entries, and create better docs. Also improve the test file for the linter significantly.