to_additive and other attributes

Stream: mathlib4

[Floris van Doorn]

There is some hacky code when we want to apply to_additive and other attributes to a declaration.
The problem we're trying to solve is the following:

• to_additive generates an additivized version of each declaration, and there is a dictionary to keep track of the (multipliciative, additive) pairs of declarations.
• Other attributes (simp, norm_cast, simps, ...) can also generate new declarations (e.g. equation lemmas)

In order for to_additive to work, the declaration-pairs generated by other attributes also need to be added to the dictionary. Currently this is done in a hacky way for simp and simps, by modifying what these attributes do (that is: run versions of the attributes that return an array of added declarations and then insert translations between those), but this is not really extendible.

I was considering a new approach: do something similar to whatsnew in: look at what declarations have been added to the environment, and just pairwise add these declarations to the dictionary.

Two questions:

• Does this seem like a reasonable approach? Is there a less hacky way to do this?
• In what way is the list returned by docs#Lean.PersistentHashMap.toList ordered? I need to make sure that if an attribute adds multiple declarations, the correct correspondences are added to the dictionary.

[Floris van Doorn]

(c.f. bug report at #1074)

[Eric Wieser]

An alternative approach would be to have a core change which adds some kind of environment hook, which allows you to run a handler whenever anything is added to the environment.