inductive Lean.Compiler.SpecializeAttributeKind : Type

• specialize : SpecializeAttributeKind
• nospecialize : SpecializeAttributeKind

instance Lean.Compiler.instInhabitedSpecializeAttributeKind : Inhabited SpecializeAttributeKind

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

@[export lean_has_specialize_attribute]

partial def Lean.Compiler.hasSpecializeAttributeOld (env : Environment) (n : Name) : Bool

@[export lean_has_nospecialize_attribute]

partial def Lean.Compiler.hasNospecializeAttributeOld (env : Environment) (n : Name) : Bool

inductive Lean.Compiler.SpecArgKind : Type

• fixed : SpecArgKind
• fixedNeutral : SpecArgKind
• fixedHO : SpecArgKind
• fixedInst : SpecArgKind
• other : SpecArgKind

instance Lean.Compiler.instInhabitedSpecArgKind : Inhabited SpecArgKind

structure Lean.Compiler.SpecInfo : Type

• mutualDecls : List Name
• argKinds : List SpecArgKind

instance Lean.Compiler.instInhabitedSpecInfo : Inhabited SpecInfo

structure Lean.Compiler.SpecState : Type

• specInfo : SMap Name SpecInfo
• cache : SMap Expr Name

instance Lean.Compiler.instInhabitedSpecState : Inhabited SpecState

inductive Lean.Compiler.SpecEntry : Type

• info (name : Name) (info : SpecInfo) : SpecEntry
• cache (key : Expr) (fn : Name) : SpecEntry

instance Lean.Compiler.instInhabitedSpecEntry : Inhabited SpecEntry

def Lean.Compiler.SpecState.addEntry (s : SpecState) (e : SpecEntry) : SpecState

def Lean.Compiler.SpecState.switch : SpecState → SpecState

opaque Lean.Compiler.specExtension : SimplePersistentEnvExtension SpecEntry SpecState

@[export lean_add_specialization_info]

def Lean.Compiler.addSpecializationInfo (env : Environment) (fn : Name) (info : SpecInfo) : Environment

@[export lean_get_specialization_info]

def Lean.Compiler.getSpecializationInfo (env : Environment) (fn : Name) : Option SpecInfo

@[export lean_cache_specialization]

def Lean.Compiler.cacheSpecialization (env : Environment) (e : Expr) (fn : Name) : Environment

@[export lean_get_cached_specialization]

def Lean.Compiler.getCachedSpecialization (env : Environment) (e : Expr) : Option Name