Lean.Compiler.Specialize

source

inductive Lean.Compiler.SpecializeAttributeKind :

Type

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

Instances For

source

instance Lean.Compiler.instInhabitedSpecializeAttributeKind :

Inhabited Lean.Compiler.SpecializeAttributeKind

source

instance Lean.Compiler.instBEqSpecializeAttributeKind :

BEq Lean.Compiler.SpecializeAttributeKind

source

opaque Lean.Compiler.nospecializeAttr :

Lean.TagAttribute

source

opaque Lean.Compiler.specializeAttr :

Lean.ParametricAttribute (Array Nat)

source

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

Option (Array Nat)

Instances For

source

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

Bool

Instances For

source

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

Bool

Instances For

source

@[export lean_has_specialize_attribute]

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

Bool

source

@[export lean_has_nospecialize_attribute]

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

Bool

source

inductive Lean.Compiler.SpecArgKind :

Type

Instances For

source

instance Lean.Compiler.instInhabitedSpecArgKind :

Inhabited Lean.Compiler.SpecArgKind

source

structure Lean.Compiler.SpecInfo :

Type

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

Instances For

source

instance Lean.Compiler.instInhabitedSpecInfo :

Inhabited Lean.Compiler.SpecInfo

source

structure Lean.Compiler.SpecState :

Type

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

Instances For

source

instance Lean.Compiler.instInhabitedSpecState :

Inhabited Lean.Compiler.SpecState

source

inductive Lean.Compiler.SpecEntry :

Type

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

Instances For

source

instance Lean.Compiler.instInhabitedSpecEntry :

Inhabited Lean.Compiler.SpecEntry

source

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

Lean.Compiler.SpecState

Instances For

source

def Lean.Compiler.SpecState.switch :

Lean.Compiler.SpecState → Lean.Compiler.SpecState

Instances For

source

opaque Lean.Compiler.specExtension :

Lean.SimplePersistentEnvExtension Lean.Compiler.SpecEntry Lean.Compiler.SpecState

source

@[export lean_add_specialization_info]

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

Lean.Environment

Instances For

source

@[export lean_get_specialization_info]

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

Option Lean.Compiler.SpecInfo

Instances For

source

@[export lean_cache_specialization]

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

Lean.Environment

Instances For

source

@[export lean_get_cached_specialization]

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

Option Lake.Name

Instances For