A helper function for constructing a related declaration from an existing one.
This is currently used by the attributes
and has been factored out to avoid code duplication.
Feel free to add features as needed for other applications.
addDeclarationRanges, so jump-to-definition works,
- copies the
protectedstatus of the existing declaration, and
- supports copying attributes.
src : Nameis the existing declaration that we are modifying.
suffix : Stringwill be appended to
srcto form the name of the new declaration.
ref : Syntaxis the syntax where the user requested the related declaration.
construct type value levels : MetaM (Expr × List Name)given the type, value, and universe variables of the original declaration, should construct the value of the new declaration, along with the names of its universe variables.
attrsis the attributes that should be applied to both the new and the original declaration, e.g. in the usage
@[reassoc (attr := simp)]. We apply it to both declarations, to have the same behavior as
to_additive, and to shorten some attribute commands. Note that
@[elementwise (attr := simp), reassoc (attr := simp)]will try to apply
simptwice to the current declaration, but that causes no issues.