@[notation_class] attribute for
This declares the
@[notation_class] attribute, which is used to give smarter default projections
We put this in a separate file so that we can already tag some declarations with this attribute
in the file where we declare
@[simps]. For further documentation, see
@[notation_class] attribute specifies that this is a notation class,
and this notation should be used instead of projections by
- This is only important if the projection is written differently using notation, e.g.
Zero.zero. We also add it to non-heterogenous notation classes, like
Neg, but it doesn't do much for any class that extends
@[notation_class * <projName> Simps.findCoercionArgs]is used to configure the
- The first name argument is the projection name we use as the key to search for this class (default: name of first projection of the class).
- The second argument is the name of a declaration that has type
findArgTypewhich is defined to be
Name → Name → Array Expr → MetaM (Array (Option Expr)). This declaration specifies how to generate the arguments of the notation class from the arguments of classes that use the projection.
- One or more equations did not get rendered due to their size.
The type of methods to find arguments for automatic projections for
We partly define this as a separate definition so that the unused arguments linter doesn't complain.
Data needed to generate automatic projections. This data is associated to a name of a projection in a structure that must be used to trigger the search.
- className : Lean.Name
classNameis the name of the class we are looking for.
- isNotation : Bool
isNotationis a boolean that specifies whether this is notation (false for the coercions
SetLike). If this is set to true, we add the current class as hypothesis during type-class synthesis.
- findArgs : Lean.Name
The method to find the arguments of the class.