inductive Lean.Compiler.SpecializeAttributeKind : Type

• specialize : SpecializeAttributeKind
• nospecialize : SpecializeAttributeKind

instance Lean.Compiler.instInhabitedSpecializeAttributeKind : Inhabited SpecializeAttributeKind

def Lean.Compiler.instInhabitedSpecializeAttributeKind.default : SpecializeAttributeKind

def Lean.Compiler.instBEqSpecializeAttributeKind.beq : SpecializeAttributeKind → SpecializeAttributeKind → Bool

instance Lean.Compiler.instBEqSpecializeAttributeKind : BEq SpecializeAttributeKind

opaque Lean.Compiler.nospecializeAttr : TagAttribute

Marks a definition to never be specialized during code generation.

opaque Lean.Compiler.specializeAttr : ParametricAttribute (Array Nat)

Marks a definition to always be specialized during code generation.

Specialization is an optimization in the code generator for generating variants of a function that are specialized to specific parameter values. This is in particular useful for functions that take other functions as parameters: Usually when passing functions as parameters, a closure needs to be allocated that will then be called. Using @[specialize] prevents both of these operations by using the provided function directly in the specialization of the inner function.

@[specialize] can take additional arguments for the parameter names or indices (starting at 1) of the parameters that should be specialized. By default, instance and function parameters are specialized.

def Lean.Compiler.getSpecializationArgs? (env : Environment) (declName : Name) : Option (Array Nat)

def Lean.Compiler.hasSpecializeAttribute (env : Environment) (declName : Name) : Bool

def Lean.Compiler.hasNospecializeAttribute (env : Environment) (declName : Name) : Bool