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 * Simps.findCoercionArgs] is used to configure the SetLike and FunLike 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
  • One or more equations did not get rendered due to their size.
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
      • One or more equations did not get rendered due to their size.
      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 (FunLike or SetLike)

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      • 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 FunLike 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.

                      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.

                      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.