inductive Lean.Compiler.SpecializeAttributeKind : Type

• specialize: Lean.Compiler.SpecializeAttributeKind
• nospecialize: Lean.Compiler.SpecializeAttributeKind

instance Lean.Compiler.instInhabitedSpecializeAttributeKind : Inhabited Lean.Compiler.SpecializeAttributeKind

Equations

• Lean.Compiler.instInhabitedSpecializeAttributeKind = { default := Lean.Compiler.SpecializeAttributeKind.specialize }

instance Lean.Compiler.instBEqSpecializeAttributeKind : BEq Lean.Compiler.SpecializeAttributeKind

Equations

• Lean.Compiler.instBEqSpecializeAttributeKind = { beq := Lean.Compiler.beqSpecializeAttributeKind✝ }

opaque Lean.Compiler.nospecializeAttr : Lean.TagAttribute

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

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

Equations

• Lean.Compiler.getSpecializationArgs? env declName = Lean.Compiler.specializeAttr.getParam? env declName

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

Equations

• Lean.Compiler.hasSpecializeAttribute env declName = (Lean.Compiler.getSpecializationArgs? env declName).isSome

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

Equations

• Lean.Compiler.hasNospecializeAttribute env declName = Lean.Compiler.nospecializeAttr.hasTag env declName

@[export lean_has_specialize_attribute]

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

@[export lean_has_nospecialize_attribute]

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

inductive Lean.Compiler.SpecArgKind : Type

• fixed: Lean.Compiler.SpecArgKind
• fixedNeutral: Lean.Compiler.SpecArgKind
• fixedHO: Lean.Compiler.SpecArgKind
• fixedInst: Lean.Compiler.SpecArgKind
• other: Lean.Compiler.SpecArgKind

instance Lean.Compiler.instInhabitedSpecArgKind : Inhabited Lean.Compiler.SpecArgKind

Equations

• Lean.Compiler.instInhabitedSpecArgKind = { default := Lean.Compiler.SpecArgKind.fixed }

structure Lean.Compiler.SpecInfo : Type

• mutualDecls : List Lake.Name
• argKinds : List Lean.Compiler.SpecArgKind

instance Lean.Compiler.instInhabitedSpecInfo : Inhabited Lean.Compiler.SpecInfo

Equations

• Lean.Compiler.instInhabitedSpecInfo = { default := { mutualDecls := default, argKinds := default } }

structure Lean.Compiler.SpecState : Type

• specInfo : Lean.SMap Lake.Name Lean.Compiler.SpecInfo
• cache : Lean.SMap Lean.Expr Lake.Name

instance Lean.Compiler.instInhabitedSpecState : Inhabited Lean.Compiler.SpecState

Equations

• Lean.Compiler.instInhabitedSpecState = { default := { specInfo := default, cache := default } }

inductive Lean.Compiler.SpecEntry : Type

• info: Lake.Name → Lean.Compiler.SpecInfo → Lean.Compiler.SpecEntry
• cache: Lean.Expr → Lake.Name → Lean.Compiler.SpecEntry

instance Lean.Compiler.instInhabitedSpecEntry : Inhabited Lean.Compiler.SpecEntry

Equations

• Lean.Compiler.instInhabitedSpecEntry = { default := Lean.Compiler.SpecEntry.info default default }

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

Equations

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

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

Equations

• x.switch = match x with | { specInfo := m₁, cache := m₂ } => { specInfo := m₁.switch, cache := m₂.switch }

opaque Lean.Compiler.specExtension : Lean.SimplePersistentEnvExtension Lean.Compiler.SpecEntry Lean.Compiler.SpecState

@[export lean_add_specialization_info]

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

Equations

• Lean.Compiler.addSpecializationInfo env fn info = Lean.PersistentEnvExtension.addEntry Lean.Compiler.specExtension env (Lean.Compiler.SpecEntry.info fn info)

@[export lean_get_specialization_info]

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

Equations

• Lean.Compiler.getSpecializationInfo env fn = (Lean.Compiler.specExtension.getState env).specInfo.find? fn

@[export lean_cache_specialization]

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

Equations

• Lean.Compiler.cacheSpecialization env e fn = Lean.PersistentEnvExtension.addEntry Lean.Compiler.specExtension env (Lean.Compiler.SpecEntry.cache e fn)

@[export lean_get_cached_specialization]

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

Equations

• Lean.Compiler.getCachedSpecialization env e = (Lean.Compiler.specExtension.getState env).cache.find? e