Documentation

Mathlib.Tactic.Simps.NotationClass

@[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. + uses HAdd.hAdd, not Add.add and 0 uses OfNat.ofNat not Zero.zero. We also add it to non-heterogenous notation classes, like Neg, but it doesn't do much for any class that extends Neg.
  • @[notation_class * <projName> Simps.findCoercionArgs] is used to configure the SetLike and DFunLike 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 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.
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 for the Zero class.

                              Equations
                                Instances For

                                  Find arguments for the One class.

                                  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 coercions DFunLike and 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.

                                          Instances For

                                            @[notation_class] attribute. Note: this is not a NameMapAttribute because we key on the argument of the attribute, not the declaration name.