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

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

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