def Lean.ModuleEnvExtension (σ : Type) : Type

Persistent environment extension for storing a single serializable value per module.

Equations

• Lean.ModuleEnvExtension σ = Lean.PersistentEnvExtension σ σ σ

def Lean.registerModuleEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) (name : Name := by exact decl_name%) : IO (ModuleEnvExtension σ)

Equations

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

instance Lean.ModuleEnvExtension.instInhabited {σ : Type} [Inhabited σ] : Inhabited (ModuleEnvExtension σ)

Equations

• Lean.ModuleEnvExtension.instInhabited = inferInstanceAs (Inhabited (Lean.PersistentEnvExtension σ σ σ))

def Lean.ModuleEnvExtension.getStateByIdx? {σ : Type} [Inhabited σ] (ext : ModuleEnvExtension σ) (env : Environment) (idx : ModuleIdx) : Option σ

Equations

• ext.getStateByIdx? env idx = (Lean.PersistentEnvExtension.getModuleEntries ext env idx)[0]?

def Lean.Environment.getModulePackageByIdx? (env : Environment) (idx : ModuleIdx) : Option PkgId

Returns the package (if any) of an imported module (by its index).

Equations

• env.getModulePackageByIdx? idx = (Lean.modPkgExt✝.getStateByIdx? env idx).join

@[inline]

def Lean.Environment.getModulePackage? (env : Environment) : Option PkgId

Returns the package (if any) of the current module.

Equations

• env.getModulePackage? = Lean.PersistentEnvExtension.getState Lean.modPkgExt✝ env

@[inline]

def Lean.Environment.setModulePackage (pkg? : Option PkgId) (env : Environment) : Environment

Sets the package of the current module.

Equations

• Lean.Environment.setModulePackage pkg? env = Lean.PersistentEnvExtension.setState Lean.modPkgExt✝ env pkg?

@[export lean_get_symbol_stem]

def Lean.getSymbolStem (env : Environment) (declName : Name) : String

Returns the standard base of the native symbol for the compiled constant declName.

For many constants, this is the full symbol. However, initializers have an additional prefix (i.e., _init_) and boxed functions have an additional suffix (i.e., ___boxed). Furthermore, some constants do not use this stem at all (e.g., main and definitions with @[export]).

Equations

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