@[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.

def notation_class : Lean.ParserDescr

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.

def Simps.findArgType : Type

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

• Simps.findArgType = (Lean.Name → Lean.Name → Array Lean.Expr → Lean.MetaM (Array (Option Lean.Expr)))

def Simps.defaultfindArgs : Simps.findArgType

Find arguments for a notation class

Equations

• One or more equations did not get rendered due to their size.

def Simps.copyFirst : Simps.findArgType

Find arguments by duplicating the first argument. Used for pow.

Equations

• Simps.copyFirst x x args = pure (Array.map some (Array.push args (Option.getD args[0]? default)))

def Simps.copySecond : Simps.findArgType

Find arguments by duplicating the first argument. Used for smul.

Equations

• Simps.copySecond x x args = pure (Array.map some (Array.push args (Option.getD args[1]? default)))

def Simps.nsmulArgs : Simps.findArgType

Find arguments by prepending ℕ and duplicating the first argument. Used for nsmul.

Equations

• Simps.nsmulArgs x x args = pure (Array.map some (#[Lean.Expr.const `Nat [], Option.getD args[0]? default] ++ args))

def Simps.zsmulArgs : Simps.findArgType

Find arguments by prepending ℤ and duplicating the first argument. Used for zsmul.

Equations

• Simps.zsmulArgs x x args = pure (Array.map some (#[Lean.Expr.const `Int [], Option.getD args[0]? default] ++ args))

def Simps.findZeroArgs : Simps.findArgType

Find arguments for the Zero class.

Equations

• Simps.findZeroArgs x x args = pure #[some (Option.getD args[0]? default), some (Lean.mkRawNatLit 0)]

def Simps.findOneArgs : Simps.findArgType

Find arguments for the One class.

Equations

• Simps.findOneArgs x x args = pure #[some (Option.getD args[0]? default), some (Lean.mkRawNatLit 1)]

def Simps.findCoercionArgs : Simps.findArgType

Find arguments of a coercion class (FunLike or SetLike)

Equations

• One or more equations did not get rendered due to their size.

structure Simps.AutomaticProjectionData : Type

• 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.

instance Simps.instInhabitedAutomaticProjectionData : Inhabited Simps.AutomaticProjectionData

Equations

• Simps.instInhabitedAutomaticProjectionData = { default := { className := default, isNotation := default, findArgs := default } }

opaque Simps.notationClassAttr : Lean.NameMapExtension Simps.AutomaticProjectionData

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