opaque Lean.EnvExtensionStateSpec : (α : Type) × Inhabited α

Opaque environment extension state.

def Lean.EnvExtensionState : Type

Equations

• Lean.EnvExtensionState = Lean.EnvExtensionStateSpec.fst

instance Lean.instInhabitedEnvExtensionState : Inhabited Lean.EnvExtensionState

Equations

• Lean.instInhabitedEnvExtensionState = Lean.EnvExtensionStateSpec.snd

def Lean.ModuleIdx : Type

Equations

• Lean.ModuleIdx = Nat

@[reducible, inline]

abbrev Lean.ModuleIdx.toNat (midx : Lean.ModuleIdx) : Nat

Equations

• midx.toNat = midx

instance Lean.instInhabitedModuleIdx : Inhabited Lean.ModuleIdx

Equations

• Lean.instInhabitedModuleIdx = { default := 0 }

@[reducible, inline]

abbrev Lean.ConstMap : Type

Equations

• Lean.ConstMap = Lean.SMap Lake.Name Lean.ConstantInfo

structure Lean.Import : Type

• module : Lake.Name
• runtimeOnly : Bool

instance Lean.instReprImport : Repr Lean.Import

Equations

• Lean.instReprImport = { reprPrec := Lean.reprImport✝ }

instance Lean.instInhabitedImport : Inhabited Lean.Import

Equations

• Lean.instInhabitedImport = { default := { module := default, runtimeOnly := default } }

instance Lean.instCoeNameImport : Coe Lake.Name Lean.Import

Equations

• Lean.instCoeNameImport = { coe := fun (x : Lake.Name) => { module := x, runtimeOnly := false } }

instance Lean.instToStringImport : ToString Lean.Import

Equations

• Lean.instToStringImport = { toString := fun (imp : Lean.Import) => toString imp.module ++ if imp.runtimeOnly = true then " (runtime)" else "" }

def Lean.CompactedRegion : Type

A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk. Objects inside the region do not have reference counters and cannot be freed individually. The contents of .olean files are compacted regions.

Equations

• Lean.CompactedRegion = USize

@[extern lean_compacted_region_is_memory_mapped]

opaque Lean.CompactedRegion.isMemoryMapped : Lean.CompactedRegion → Bool

@[extern lean_compacted_region_free]

unsafe opaque Lean.CompactedRegion.free : Lean.CompactedRegion → IO Unit

Free a compacted region and its contents. No live references to the contents may exist at the time of invocation.

opaque Lean.EnvExtensionEntrySpec : NonemptyType

Opaque persistent environment extension entry.

def Lean.EnvExtensionEntry : Type

Equations

• Lean.EnvExtensionEntry = Lean.EnvExtensionEntrySpec.type

instance Lean.instNonemptyEnvExtensionEntry : Nonempty Lean.EnvExtensionEntry

Equations

• Lean.instNonemptyEnvExtensionEntry = ⋯

structure Lean.ModuleData : Type

Content of a .olean file. We use compact.cpp to generate the image of this object in disk.

• imports : Array Lean.Import
• constNames : Array Lake.Name

  constNames contains all constant names in constants. This information is redundant. It is equal to constants.map fun c => c.name, but it improves the performance of importModules. perf reports that 12% of the runtime was being spent on ConstantInfo.name when importing a file containing only import Lean

• constants : Array Lean.ConstantInfo
• extraConstNames : Array Lake.Name

  Extra entries for the const2ModIdx map in the Environment object. The code generator creates auxiliary declarations that are not in the mapping constants, but we want to know in which module they were generated.

• entries : Array (Lake.Name × Array Lean.EnvExtensionEntry)

instance Lean.instInhabitedModuleData : Inhabited Lean.ModuleData

Equations

• Lean.instInhabitedModuleData = { default := { imports := default, constNames := default, constants := default, extraConstNames := default, entries := default } }

structure Lean.EnvironmentHeader : Type

Environment fields that are not used often.

• trustLevel : UInt32

  The trust level used by the kernel. For example, the kernel assumes imported constants are type correct when the trust level is greater than zero.

• quotInit : Bool

  quotInit = true if the command init_quot has already been executed for the environment, and Quot declarations have been added to the environment.

• mainModule : Lake.Name

  Name of the module being compiled.

• imports : Array Lean.Import

  Direct imports

• regions : Array Lean.CompactedRegion

  Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management.

• moduleNames : Array Lake.Name

  Name of all imported modules (directly and indirectly).

• moduleData : Array Lean.ModuleData

  Module data for all imported modules.

instance Lean.instNonemptyEnvironmentHeader : Nonempty Lean.EnvironmentHeader

Equations

• Lean.instNonemptyEnvironmentHeader = ⋯

structure Lean.Environment : Type

An environment stores declarations provided by the user. The kernel currently supports different kinds of declarations such as definitions, theorems, and inductive families. Each has a unique identifier (i.e., Name), and can be parameterized by a sequence of universe parameters. A constant in Lean is just a reference to a ConstantInfo object. The main task of the kernel is to type check these declarations and refuse type incorrect ones. The kernel does not allow declarations containing metavariables and/or free variables to be added to an environment. Environments are never destructively updated.

The environment also contains a collection of extensions. For example, the simp theorems declared by users are stored in an environment extension. Users can declare new extensions using meta-programming.

• const2ModIdx : Std.HashMap Lake.Name Lean.ModuleIdx

  Mapping from constant name to module (index) where constant has been declared. Recall that a Lean file has a header where previously compiled modules can be imported. Each imported module has a unique ModuleIdx. Many extensions use the ModuleIdx to efficiently retrieve information stored in imported modules.

  Remark: this mapping also contains auxiliary constants, created by the code generator, that are not in the field constants. These auxiliary constants are invisible to the Lean kernel and elaborator. Only the code generator uses them.

• constants : Lean.ConstMap

  Mapping from constant name to ConstantInfo. It contains all constants (definitions, theorems, axioms, etc) that have been already type checked by the kernel.

• extensions : Array Lean.EnvExtensionState

  Environment extensions. It also includes user-defined extensions.

• extraConstNames : Lean.NameSet

  Constant names to be saved in the field extraConstNames at ModuleData. It contains auxiliary declaration names created by the code generator which are not in constants. When importing modules, we want to insert them at const2ModIdx.

• header : Lean.EnvironmentHeader

  The header contains additional information that is not updated often.

instance Lean.instNonemptyEnvironment : Nonempty Lean.Environment

Equations

• Lean.instNonemptyEnvironment = ⋯

def Lean.Environment.addExtraName (env : Lean.Environment) (name : Lake.Name) : Lean.Environment

Save an extra constant name that is used to populate const2ModIdx when we import .olean files. We use this feature to save in which module an auxiliary declaration created by the code generator has been created.

Equations

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

@[export lean_environment_find]

def Lean.Environment.find? (env : Lean.Environment) (n : Lake.Name) : Option Lean.ConstantInfo

Equations

• env.find? n = Lean.SMap.find?' env.constants n

def Lean.Environment.contains (env : Lean.Environment) (n : Lake.Name) : Bool

Equations

• env.contains n = Lean.SMap.contains env.constants n

def Lean.Environment.imports (env : Lean.Environment) : Array Lean.Import

Equations

• env.imports = env.header.imports

def Lean.Environment.allImportedModuleNames (env : Lean.Environment) : Array Lake.Name

Equations

• env.allImportedModuleNames = env.header.moduleNames

@[export lean_environment_set_main_module]

def Lean.Environment.setMainModule (env : Lean.Environment) (m : Lake.Name) : Lean.Environment

Equations

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

@[export lean_environment_main_module]

def Lean.Environment.mainModule (env : Lean.Environment) : Lake.Name

Equations

• env.mainModule = env.header.mainModule

def Lean.Environment.getModuleIdxFor? (env : Lean.Environment) (declName : Lake.Name) : Option Lean.ModuleIdx

Equations

• env.getModuleIdxFor? declName = env.const2ModIdx[declName]?

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

Equations

• env.isConstructor declName = match env.find? declName with | some (Lean.ConstantInfo.ctorInfo val) => true | x => false

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

Equations

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

def Lean.Environment.getModuleIdx? (env : Lean.Environment) (moduleName : Lake.Name) : Option Lean.ModuleIdx

Equations

• env.getModuleIdx? moduleName = env.header.moduleNames.findIdx? fun (x : Lake.Name) => x == moduleName

inductive Lean.KernelException : Type

Exceptions that can be raised by the Kernel when type checking new declarations.

• unknownConstant: Lean.Environment → Lake.Name → Lean.KernelException
• alreadyDeclared: Lean.Environment → Lake.Name → Lean.KernelException
• declTypeMismatch: Lean.Environment → Lean.Declaration → Lean.Expr → Lean.KernelException
• declHasMVars: Lean.Environment → Lake.Name → Lean.Expr → Lean.KernelException
• declHasFVars: Lean.Environment → Lake.Name → Lean.Expr → Lean.KernelException
• funExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
• typeExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
• letTypeMismatch: Lean.Environment → Lean.LocalContext → Lake.Name → Lean.Expr → Lean.Expr → Lean.KernelException
• exprTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.KernelException
• appTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.Expr → Lean.KernelException
• invalidProj: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
• thmTypeIsNotProp: Lean.Environment → Lake.Name → Lean.Expr → Lean.KernelException
• other: String → Lean.KernelException
• deterministicTimeout: Lean.KernelException
• excessiveMemory: Lean.KernelException
• deepRecursion: Lean.KernelException
• interrupted: Lean.KernelException

@[extern lean_add_decl]

opaque Lean.Environment.addDeclCore (env : Lean.Environment) (maxHeartbeats : USize) (decl : Lean.Declaration) (cancelTk? : Option IO.CancelToken) : Except Lean.KernelException Lean.Environment

Type check given declaration and add it to the environment

@[extern lean_add_decl_without_checking]

opaque Lean.Environment.addDeclWithoutChecking (env : Lean.Environment) (decl : Lean.Declaration) : Except Lean.KernelException Lean.Environment

Add declaration to kernel without type checking it. WARNING This function is meant for temporarily working around kernel performance issues. It compromises soundness because, for example, a buggy tactic may produce an invalid proof, and the kernel will not catch it if the new option is set to true.

def Lean.ConstantInfo.instantiateTypeLevelParams (c : Lean.ConstantInfo) (ls : List Lean.Level) : Lean.Expr

Equations

• c.instantiateTypeLevelParams ls = c.type.instantiateLevelParams c.levelParams ls

def Lean.ConstantInfo.instantiateValueLevelParams! (c : Lean.ConstantInfo) (ls : List Lean.Level) : Lean.Expr

Equations

• c.instantiateValueLevelParams! ls = c.value!.instantiateLevelParams c.levelParams ls

structure Lean.EnvExtensionInterface : Type 1

Interface for managing environment extensions.

• ext : Type → Type
• inhabitedExt : {σ : Type} → Inhabited σ → Inhabited (self.ext σ)
• registerExt : {σ : Type} → IO σ → IO (self.ext σ)
• setState : {σ : Type} → self.ext σ → Array Lean.EnvExtensionState → σ → Array Lean.EnvExtensionState
• modifyState : {σ : Type} → self.ext σ → Array Lean.EnvExtensionState → (σ → σ) → Array Lean.EnvExtensionState
• getState : {σ : Type} → [inst : Inhabited σ] → self.ext σ → Array Lean.EnvExtensionState → σ
• mkInitialExtStates : IO (Array Lean.EnvExtensionState)
• ensureExtensionsSize : Array Lean.EnvExtensionState → IO (Array Lean.EnvExtensionState)

instance Lean.instInhabitedEnvExtensionInterface : Inhabited Lean.EnvExtensionInterface

Equations

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

Unsafe implementation of EnvExtensionInterface

structure Lean.EnvExtensionInterfaceUnsafe.Ext (σ : Type) : Type

• idx : Nat
• mkInitial : IO σ

instance Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt : {a : Type} → Inhabited (Lean.EnvExtensionInterfaceUnsafe.Ext a)

Equations

• Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt = { default := { idx := default, mkInitial := default } }

def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize (exts : Array Lean.EnvExtensionState) : IO (Array Lean.EnvExtensionState)

User-defined environment extensions are declared using the initialize command. This command is just syntax sugar for the init attribute. When we import lean modules, the vector stored at envExtensionsRef may increase in size because of user-defined environment extensions. When this happens, we must adjust the size of the env.extensions. This method is invoked when processing imports.

Equations

• Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize exts = Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop exts.size exts

partial def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop (i : Nat) (exts : Array Lean.EnvExtensionState) : IO (Array Lean.EnvExtensionState)

unsafe def Lean.EnvExtensionInterfaceUnsafe.setState {σ : Type} (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (exts : Array Lean.EnvExtensionState) (s : σ) : Array Lean.EnvExtensionState

@[inline]

unsafe def Lean.EnvExtensionInterfaceUnsafe.modifyState {σ : Type} (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (exts : Array Lean.EnvExtensionState) (f : σ → σ) : Array Lean.EnvExtensionState

unsafe def Lean.EnvExtensionInterfaceUnsafe.getState {σ : Type} [Inhabited σ] (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (exts : Array Lean.EnvExtensionState) : σ

unsafe def Lean.EnvExtensionInterfaceUnsafe.registerExt {σ : Type} (mkInitial : IO σ) : IO (Lean.EnvExtensionInterfaceUnsafe.Ext σ)

def Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates : IO (Array Lean.EnvExtensionState)

Equations

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

unsafe def Lean.EnvExtensionInterfaceUnsafe.imp : Lean.EnvExtensionInterface

@[implemented_by Lean.EnvExtensionInterfaceUnsafe.imp]

opaque Lean.EnvExtensionInterfaceImp : Lean.EnvExtensionInterface

def Lean.EnvExtension (σ : Type) : Type

Equations

• Lean.EnvExtension σ = Lean.EnvExtensionInterfaceImp.ext σ

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

Equations

• Lean.EnvExtension.instInhabited = Lean.EnvExtensionInterfaceImp.inhabitedExt s

def Lean.EnvExtension.setState {σ : Type} (ext : Lean.EnvExtension σ) (env : Lean.Environment) (s : σ) : Lean.Environment

Equations

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

def Lean.EnvExtension.modifyState {σ : Type} (ext : Lean.EnvExtension σ) (env : Lean.Environment) (f : σ → σ) : Lean.Environment

Equations

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

def Lean.EnvExtension.getState {σ : Type} [Inhabited σ] (ext : Lean.EnvExtension σ) (env : Lean.Environment) : σ

Equations

• ext.getState env = Lean.EnvExtensionInterfaceImp.getState ext env.extensions

def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) : IO (Lean.EnvExtension σ)

Environment extensions can only be registered during initialization. Reasons: 1- Our implementation assumes the number of extensions does not change after an environment object is created. 2- We do not use any synchronization primitive to access envExtensionsRef.

Note that by default, extension state is not stored in .olean files and will not propagate across imports. For that, you need to register a persistent environment extension.

Equations

• Lean.registerEnvExtension mkInitial = Lean.EnvExtensionInterfaceImp.registerExt mkInitial

@[export lean_mk_empty_environment]

def Lean.mkEmptyEnvironment (trustLevel : optParam UInt32 0) : IO Lean.Environment

Equations

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

structure Lean.PersistentEnvExtensionState (α : Type) (σ : Type) : Type

• importedEntries : Array (Array α)
• state : σ

structure Lean.ImportM.Context : Type

• env : Lean.Environment
• opts : Lean.Options

@[reducible, inline]

abbrev Lean.ImportM (α : Type) : Type

Equations

• Lean.ImportM = ReaderT Lean.ImportM.Context IO

structure Lean.PersistentEnvExtension (α : Type) (β : Type) (σ : Type) : Type

An environment extension with support for storing/retrieving entries from a .olean file.

• α is the type of the entries that are stored in .olean files.
• β is the type of values used to update the state.
• σ is the actual state.

For most extensions, α and β coincide. α and ‵β` do not coincide for extensions where the data used to update the state contains elements which cannot be stored in files (for example, closures).

During elaboration of a module, state of type σ can be both read and written. When elaboration is complete, the state of type σ is converted to serialized state of type Array α by exportEntriesFn. To read the current module's state, use PersistentEnvExtension.getState. To modify it, use PersistentEnvExtension.addEntry, with an addEntryFn that performs the appropriate modification.

When a module is loaded, the values saved by all of its dependencies for this PersistentEnvExtension are available as an Array (Array α) via the environment extension, with one array per transitively imported module. The state of type σ used in the current module can be initialized from these imports by specifying a suitable addImportedFn. The addImportedFn runs at the beginning of elaboration for every module, so it's usually better for performance to query the array of imported modules directly, because only a fraction of imported entries is usually queried during elaboration of a module.

The most typical pattern for using PersistentEnvExtension is to set σ to a datatype such as NameMap that efficiently tracks data for the current module. Then, in exportEntriesFn, this type is converted to an array of pairs, sorted by the key. Given ext : PersistentEnvExtension α β σ and env : Environment, the complete array of imported entries sorted by module index can be obtained using (ext.toEnvExtension.getState env).importedEntries. To query the extension for some constant name n, first use env.getModuleIdxFor? n. If it returns none, look up n in the current module's state (the NameMap). If it returns some idx, use ext.getModuleEntries env idx to get the array of entries for n's defining module, and query it using Array.binSearch. This pattern imposes a constraint that the extension can only track metadata that is declared in the same module as the definition to which it applies; relaxing this restriction can make queries slower due to needing to search all modules. If it is necessary to search all modules, it is usually better to initialize the state of type σ once from all imported entries and choose a more efficient search datastructure for it.

Note that addEntryFn is not in IO. This is intentional, and allows us to write simple functions such as

def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
aliasExtension.addEntry env (a, e)

without using IO. We have many functions like addAlias.

• toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)
• name : Lake.Name
• addImportedFn : Array (Array α) → Lean.ImportM σ
• addEntryFn : σ → β → σ
• exportEntriesFn : σ → Array α
• statsFn : σ → Lean.Format

instance Lean.instInhabitedPersistentEnvExtensionState {α : Type} {σ : Type} [Inhabited σ] : Inhabited (Lean.PersistentEnvExtensionState α σ)

Equations

• Lean.instInhabitedPersistentEnvExtensionState = { default := { importedEntries := #[], state := default } }

instance Lean.instInhabitedPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [Inhabited σ] : Inhabited (Lean.PersistentEnvExtension α β σ)

Equations

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

def Lean.PersistentEnvExtension.getModuleEntries {α : Type} {β : Type} {σ : Type} [Inhabited σ] (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (m : Lean.ModuleIdx) : Array α

Equations

• ext.getModuleEntries env m = (ext.toEnvExtension.getState env).importedEntries.get! m

def Lean.PersistentEnvExtension.addEntry {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (b : β) : Lean.Environment

Equations

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

def Lean.PersistentEnvExtension.getState {α : Type} {β : Type} {σ : Type} [Inhabited σ] (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) : σ

Get the current state of the given extension in the given environment.

Equations

• ext.getState env = (ext.toEnvExtension.getState env).state

def Lean.PersistentEnvExtension.setState {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (s : σ) : Lean.Environment

Set the current state of the given extension in the given environment.

Equations

• ext.setState env s = ext.toEnvExtension.modifyState env fun (ps : Lean.PersistentEnvExtensionState α σ) => { importedEntries := ps.importedEntries, state := s }

def Lean.PersistentEnvExtension.modifyState {α : Type} {β : Type} {σ : Type} (ext : Lean.PersistentEnvExtension α β σ) (env : Lean.Environment) (f : σ → σ) : Lean.Environment

Modify the state of the given extension in the given environment by applying the given function.

Equations

• ext.modifyState env f = ext.toEnvExtension.modifyState env fun (ps : Lean.PersistentEnvExtensionState α σ) => { importedEntries := ps.importedEntries, state := f ps.state }

opaque Lean.persistentEnvExtensionsRef : IO.Ref (Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))

structure Lean.PersistentEnvExtensionDescr (α : Type) (β : Type) (σ : Type) : Type

• name : Lake.Name
• mkInitial : IO σ
• addImportedFn : Array (Array α) → Lean.ImportM σ
• addEntryFn : σ → β → σ
• exportEntriesFn : σ → Array α
• statsFn : σ → Lean.Format

unsafe def Lean.registerPersistentEnvExtensionUnsafe {α : Type} {β : Type} {σ : Type} [Inhabited σ] (descr : Lean.PersistentEnvExtensionDescr α β σ) : IO (Lean.PersistentEnvExtension α β σ)

@[implemented_by Lean.registerPersistentEnvExtensionUnsafe]

opaque Lean.registerPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [Inhabited σ] (descr : Lean.PersistentEnvExtensionDescr α β σ) : IO (Lean.PersistentEnvExtension α β σ)

def Lean.SimplePersistentEnvExtension (α : Type) (σ : Type) : Type

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

Equations

• Lean.SimplePersistentEnvExtension α σ = Lean.PersistentEnvExtension α α (List α × σ)

@[specialize #[]]

def Lean.mkStateFromImportedEntries {α : Type} {σ : Type} (addEntryFn : σ → α → σ) (initState : σ) (as : Array (Array α)) : σ

Equations

• Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun (r : σ) (es : Array α) => Array.foldl (fun (r : σ) (e : α) => addEntryFn r e) r es) initState as

structure Lean.SimplePersistentEnvExtensionDescr (α : Type) (σ : Type) : Type

• name : Lake.Name
• addEntryFn : σ → α → σ
• addImportedFn : Array (Array α) → σ
• toArrayFn : List α → Array α

def Lean.registerSimplePersistentEnvExtension {α : Type} {σ : Type} [Inhabited σ] (descr : Lean.SimplePersistentEnvExtensionDescr α σ) : IO (Lean.SimplePersistentEnvExtension α σ)

Equations

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

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

Equations

• Lean.SimplePersistentEnvExtension.instInhabited = inferInstanceAs (Inhabited (Lean.PersistentEnvExtension α α (List α × σ)))

def Lean.SimplePersistentEnvExtension.getEntries {α : Type} {σ : Type} [Inhabited σ] (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) : List α

Get the list of values used to update the state of the given SimplePersistentEnvExtension in the current file.

Equations

• ext.getEntries env = (Lean.PersistentEnvExtension.getState ext env).fst

def Lean.SimplePersistentEnvExtension.getState {α : Type} {σ : Type} [Inhabited σ] (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) : σ

Get the current state of the given SimplePersistentEnvExtension.

Equations

• ext.getState env = (Lean.PersistentEnvExtension.getState ext env).snd

def Lean.SimplePersistentEnvExtension.setState {α : Type} {σ : Type} (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) (s : σ) : Lean.Environment

Set the current state of the given SimplePersistentEnvExtension. This change is not persisted across files.

Equations

• ext.setState env s = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, snd) => (entries, s)

def Lean.SimplePersistentEnvExtension.modifyState {α : Type} {σ : Type} (ext : Lean.SimplePersistentEnvExtension α σ) (env : Lean.Environment) (f : σ → σ) : Lean.Environment

Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.

Equations

• ext.modifyState env f = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, s) => (entries, f s)

def Lean.TagDeclarationExtension : Type

Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.

Equations

• Lean.TagDeclarationExtension = Lean.SimplePersistentEnvExtension Lake.Name Lean.NameSet

def Lean.mkTagDeclarationExtension (name : autoParam Lake.Name _auto✝) : IO Lean.TagDeclarationExtension

Equations

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

instance Lean.TagDeclarationExtension.instInhabited : Inhabited Lean.TagDeclarationExtension

Equations

• Lean.TagDeclarationExtension.instInhabited = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension Lake.Name Lean.NameSet))

def Lean.TagDeclarationExtension.tag (ext : Lean.TagDeclarationExtension) (env : Lean.Environment) (declName : Lake.Name) : Lean.Environment

Equations

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

def Lean.TagDeclarationExtension.isTagged (ext : Lean.TagDeclarationExtension) (env : Lean.Environment) (declName : Lake.Name) : Bool

Equations

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

def Lean.MapDeclarationExtension (α : Type) : Type

Environment extension for mapping declarations to values. Declarations must only be inserted into the mapping in the module where they were declared.

Equations

• Lean.MapDeclarationExtension α = Lean.SimplePersistentEnvExtension (Lake.Name × α) (Lake.NameMap α)

def Lean.mkMapDeclarationExtension {α : Type} (name : autoParam Lake.Name _auto✝) : IO (Lean.MapDeclarationExtension α)

Equations

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

instance Lean.MapDeclarationExtension.instInhabited {α : Type} : Inhabited (Lean.MapDeclarationExtension α)

Equations

• Lean.MapDeclarationExtension.instInhabited = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension (Lake.Name × α) (Lake.NameMap α)))

def Lean.MapDeclarationExtension.insert {α : Type} (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lake.Name) (val : α) : Lean.Environment

Equations

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

def Lean.MapDeclarationExtension.find? {α : Type} [Inhabited α] (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lake.Name) : Option α

Equations

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

def Lean.MapDeclarationExtension.contains {α : Type} [Inhabited α] (ext : Lean.MapDeclarationExtension α) (env : Lean.Environment) (declName : Lake.Name) : Bool

Equations

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

@[extern lean_save_module_data]

opaque Lean.saveModuleData (fname : Lake.FilePath) (mod : Lake.Name) (data : Lean.ModuleData) : IO Unit

@[extern lean_read_module_data]

opaque Lean.readModuleData (fname : Lake.FilePath) : IO (Lean.ModuleData × Lean.CompactedRegion)

@[noinline, export lean_environment_free_regions]

unsafe def Lean.Environment.freeRegions (env : Lean.Environment) : IO Unit

Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in particular, env should be the last reference to any Environment derived from these imports.

def Lean.mkModuleData (env : Lean.Environment) : IO Lean.ModuleData

Equations

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

@[export lean_write_module]

def Lean.writeModule (env : Lean.Environment) (fname : Lake.FilePath) : IO Unit

Equations

• Lean.writeModule env fname = do let __do_lift ← Lean.mkModuleData env Lean.saveModuleData fname env.mainModule __do_lift

def Lean.mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Lake.Name Nat)

Construct a mapping from persistent extension name to extension index at the array of persistent extensions. We only consider extensions starting with index >= startingAt.

Equations

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

@[extern 2 lean_update_env_attributes]

opaque Lean.updateEnvAttributes : Lean.Environment → IO Lean.Environment

"Forward declaration" needed for updating the attribute table with user-defined attributes. User-defined attributes are declared using the initialize command. The initialize command is just syntax sugar for the init attribute. The init attribute is initialized after the attributeExtension is initialized. We cannot change the order since the init attribute is an attribute, and requires this extension. The attributeExtension initializer uses attributeMapRef to initialize the attribute mapping. When we a new user-defined attribute declaration is imported, attributeMapRef is updated. Later, we set this method with code that adds the user-defined attributes that were imported after we initialized attributeExtension.

@[extern 1 lean_get_num_attributes]

opaque Lean.getNumBuiltinAttributes : IO Nat

"Forward declaration" for retrieving the number of builtin attributes.

structure Lean.ImportState : Type

• moduleNameSet : Lean.NameHashSet
• moduleNames : Array Lake.Name
• moduleData : Array Lean.ModuleData
• regions : Array Lean.CompactedRegion

def Lean.throwAlreadyImported {α : Type} (s : Lean.ImportState) (const2ModIdx : Std.HashMap Lake.Name Lean.ModuleIdx) (modIdx : Nat) (cname : Lake.Name) : IO α

Equations

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

@[reducible, inline]

abbrev Lean.ImportStateM (α : Type) : Type

Equations

• Lean.ImportStateM = StateRefT' IO.RealWorld Lean.ImportState IO

@[inline]

def Lean.ImportStateM.run {α : Type} (x : Lean.ImportStateM α) (s : optParam Lean.ImportState { moduleNameSet := ∅, moduleNames := #[], moduleData := #[], regions := #[] }) : IO (α × Lean.ImportState)

Equations

• x.run s = StateRefT'.run x s

partial def Lean.importModulesCore (imports : Array Lean.Import) : Lean.ImportStateM Unit

def Lean.finalizeImport (s : Lean.ImportState) (imports : Array Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) (leakEnv : optParam Bool false) : IO Lean.Environment

Construct environment from importModulesCore results.

If leakEnv is true, we mark the environment as persistent, which means it will not be freed. We set this when the object would survive until the end of the process anyway. In exchange, RC updates are avoided, which is especially important when they would be atomic because the environment is shared across threads (potentially, storing it in an IO.Ref is sufficient for marking it as such).

Equations

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

@[export lean_import_modules]

def Lean.importModules (imports : Array Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) (leakEnv : optParam Bool false) : IO Lean.Environment

Equations

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

unsafe def Lean.withImportModules {α : Type} (imports : Array Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) (act : Lean.Environment → IO α) : IO α

Create environment object from imports and free compacted regions after calling act. No live references to the environment object or imported objects may exist after act finishes.

opaque Lean.namespacesExt : Lean.SimplePersistentEnvExtension Lake.Name Lean.NameSSet

Environment extension for tracking all namespace declared by users.

structure Lean.Kernel.Diagnostics : Type

• unfoldCounter : Lean.PHashMap Lake.Name Nat

  Number of times each declaration has been unfolded by the kernel.

• enabled : Bool

  If enabled = true, kernel records declarations that have been unfolded.

instance Lean.Kernel.instInhabitedDiagnostics : Inhabited Lean.Kernel.Diagnostics

Equations

• Lean.Kernel.instInhabitedDiagnostics = { default := { unfoldCounter := default, enabled := default } }

opaque Lean.diagExt : Lean.EnvExtension Lean.Kernel.Diagnostics

Extension for storting diagnostic information.

Remark: We store kernel diagnostic information in an environment extension to simplify the interface with the kernel implemented in C/C++. Thus, we can only track declarations in methods, such as addDecl, which return a new environment. Kernel.isDefEq and Kernel.whnf do not update the statistics. We claim this is ok since these methods are mainly used for debugging.

@[export lean_kernel_diag_is_enabled]

def Lean.Kernel.Diagnostics.isEnabled (d : Lean.Kernel.Diagnostics) : Bool

Equations

• d.isEnabled = d.enabled

def Lean.Kernel.enableDiag (env : Lean.Environment) (flag : Bool) : Lean.Environment

Enables/disables kernel diagnostics.

Equations

• Lean.Kernel.enableDiag env flag = Lean.diagExt.modifyState env fun (s : Lean.Kernel.Diagnostics) => { unfoldCounter := s.unfoldCounter, enabled := flag }

def Lean.Kernel.isDiagnosticsEnabled (env : Lean.Environment) : Bool

Equations

• Lean.Kernel.isDiagnosticsEnabled env = (Lean.diagExt.getState env).enabled

def Lean.Kernel.resetDiag (env : Lean.Environment) : Lean.Environment

Equations

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

@[export lean_kernel_record_unfold]

def Lean.Kernel.Diagnostics.recordUnfold (d : Lean.Kernel.Diagnostics) (declName : Lake.Name) : Lean.Kernel.Diagnostics

Equations

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

@[export lean_kernel_get_diag]

def Lean.Kernel.getDiagnostics (env : Lean.Environment) : Lean.Kernel.Diagnostics

Equations

• Lean.Kernel.getDiagnostics env = Lean.diagExt.getState env

@[export lean_kernel_set_diag]

def Lean.Kernel.setDiagnostics (env : Lean.Environment) (diag : Lean.Kernel.Diagnostics) : Lean.Environment

Equations

• Lean.Kernel.setDiagnostics env diag = Lean.diagExt.setState env diag

def Lean.Environment.registerNamespace (env : Lean.Environment) (n : Lake.Name) : Lean.Environment

Register a new namespace in the environment.

Equations

• env.registerNamespace n = if (Lean.namespacesExt.getState env).contains n = true then env else Lean.PersistentEnvExtension.addEntry Lean.namespacesExt env n

def Lean.Environment.isNamespace (env : Lean.Environment) (n : Lake.Name) : Bool

Return true if n is the name of a namespace in env.

Equations

• env.isNamespace n = (Lean.namespacesExt.getState env).contains n

def Lean.Environment.getNamespaceSet (env : Lean.Environment) : Lean.NameSSet

Return a set containing all namespaces in env.

Equations

• env.getNamespaceSet = Lean.namespacesExt.getState env

@[export lean_display_stats]

def Lean.Environment.displayStats (env : Lean.Environment) : IO Unit

Equations

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

@[extern lean_eval_const]

unsafe opaque Lean.Environment.evalConst (α : Type u_1) (env : Lean.Environment) (opts : Lean.Options) (constName : Lake.Name) : Except String α

Evaluate the given declaration under the given environment to a value of the given type. This function is only safe to use if the type matches the declaration's type in the environment and if enableInitializersExecution has been used before importing any modules.

unsafe def Lean.Environment.evalConstCheck (α : Type) (env : Lean.Environment) (opts : Lean.Options) (typeName : Lake.Name) (constName : Lake.Name) : ExceptT String Id α

Like evalConst, but first check that constName indeed is a declaration of type typeName. Note that this function cannot guarantee that typeName is in fact the name of the type α.

def Lean.Environment.hasUnsafe (env : Lean.Environment) (e : Lean.Expr) : Bool

Equations

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

Kernel API

@[extern lean_kernel_is_def_eq]

opaque Lean.Kernel.isDefEq (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) (b : Lean.Expr) : Except Lean.KernelException Bool

Kernel isDefEq predicate. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

def Lean.Kernel.isDefEqGuarded (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) (b : Lean.Expr) : Bool

Equations

• Lean.Kernel.isDefEqGuarded env lctx a b = match Lean.Kernel.isDefEq env lctx a b with | Except.ok result => result | x => false

@[extern lean_kernel_whnf]

opaque Lean.Kernel.whnf (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) : Except Lean.KernelException Lean.Expr

Kernel WHNF function. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

@[extern lean_kernel_check]

opaque Lean.Kernel.check (env : Lean.Environment) (lctx : Lean.LocalContext) (a : Lean.Expr) : Except Lean.KernelException Lean.Expr

Kernel typecheck function. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

class Lean.MonadEnv (m : Type → Type) : Type

• getEnv : m Lean.Environment
• modifyEnv : (Lean.Environment → Lean.Environment) → m Unit

@[always_inline]

instance Lean.instMonadEnvOfMonadLift (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.MonadEnv m] : Lean.MonadEnv n

Equations

• Lean.instMonadEnvOfMonadLift m n = { getEnv := liftM Lean.getEnv, modifyEnv := fun (f : Lean.Environment → Lean.Environment) => liftM (Lean.modifyEnv f) }

def Lean.mkDefinitionValInferrringUnsafe {m : Type → Type} [Monad m] [Lean.MonadEnv m] (name : Lake.Name) (levelParams : List Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (hints : Lean.ReducibilityHints) : m Lean.DefinitionVal

Constructs a DefinitionVal, inferring the unsafe field

Equations

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