@[notation_class]
attribute for @[simps]
#
This declares the @[notation_class]
attribute, which is used to give smarter default projections
for @[simps]
.
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 Tactic.Simps.Basic
.
The @[notation_class]
attribute specifies that this is a notation class,
and this notation should be used instead of projections by @[simps]
.
- This is only important if the projection is written differently using notation, e.g.
+
usesHAdd.hAdd
, notAdd.add
and0
usesOfNat.ofNat
notZero.zero
. We also add it to non-heterogenous notation classes, likeNeg
, but it doesn't do much for any class that extendsNeg
. @[notation_class * <projName> Simps.findCoercionArgs]
is used to configure theSetLike
andDFunLike
coercions.- 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
findArgType
which is defined to beName → 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.
Equations
Instances For
The type of methods to find arguments for automatic projections for simps
.
We partly define this as a separate definition so that the unused arguments linter doesn't complain.
Equations
Instances For
Find arguments for a notation class
Equations
Instances For
Find arguments by duplicating the first argument. Used for pow
.
Equations
Instances For
Find arguments by duplicating the first argument. Used for smul
.
Equations
Instances For
Find arguments by prepending ℕ
and duplicating the first argument. Used for nsmul
.
Equations
Instances For
Find arguments by prepending ℤ
and duplicating the first argument. Used for zsmul
.
Equations
Instances For
Find arguments of a coercion class (DFunLike
or SetLike
)
Equations
Instances For
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
className
is the name of the class we are looking for. - isNotation : Bool
isNotation
is a boolean that specifies whether this is notation (false for the coercionsDFunLike
andSetLike
). 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.
Instances For
Equations
@[notation_class]
attribute. Note: this is not a NameMapAttribute
because we key on the
argument of the attribute, not the declaration name.