def Lean.ModuleEnvExtension (σ : Type) : Type

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

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

@[instance_reducible]

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

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

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

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

@[inline]

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

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

@[inline]

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

Sets the package of the current module.

@[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 (see mkMangledBoxedName). Furthermore, some constants do not use this stem at all (e.g., main and definitions with @[export]).