Note [Environment Branches]

The kernel environment type Lean.Kernel.Environment enforces a linear order on the addition of declarations: addDeclCore takes an environment and returns a new one, assuming type checking succeeded. On the other hand, the metaprogramming-level Lean.Environment wrapper must allow for branching environment transformations so that multiple declarations can be elaborated concurrently while still being able to access information about preceding declarations that have also been branched out as soon as they are available.

The basic function to introduce such branches is addConstAsync, which takes an environment and returns a structure containing two environments: one for the "main" branch that can be used in further branching and eventually contains all the declarations of the file and one for the "async" branch that can be used concurrently to the main branch to elaborate and add the declaration for which the branch was introduced. Branches are "joined" back together implicitly via the kernel environment, which as mentioned cannot be changed concurrently: when the main branch first tries to access it, evaluation is blocked until the kernel environment on the async branch is complete. Thus adding two declarations A and B concurrently can be visualized like this:

o addConstAsync A
|\
| \
|  \
o addConstAsync B
|\   \
| \   o elaborate A
|  \  |
|   o elaborate B
|   | |
|   | o addDeclCore A
|   |/
|   o addDeclCore B
|  /
| /
|/
o .olean serialization calls Environment.toKernelEnv

While each edge represents a Lean.Environment that has its own view of the state of the module, the kernel environment really lives only in the right-most path, with all other paths merely holding an unfulfilled Task representing it and where forcing that task leads to the back-edges joining paths back together.

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

Opaque environment extension state.

def Lean.EnvExtensionState : Type

Equations

• Lean.EnvExtensionState = Lean.EnvExtensionStateSpec.fst

instance Lean.instInhabitedEnvExtensionState : Inhabited EnvExtensionState

Equations

• Lean.instInhabitedEnvExtensionState = Lean.EnvExtensionStateSpec.snd

def Lean.ModuleIdx : Type

Equations

• Lean.ModuleIdx = Nat

instance Lean.instModuleIdxBEq : BEq ModuleIdx

Equations

• Lean.instModuleIdxBEq = instBEqOfDecidableEq

instance Lean.instModuleIdxToString : ToString ModuleIdx

Equations

• Lean.instModuleIdxToString = instToStringNat

@[reducible, inline]

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

Equations

• midx.toNat = midx

instance Lean.instInhabitedModuleIdx : Inhabited ModuleIdx

Equations

• Lean.instInhabitedModuleIdx = { default := 0 }

@[reducible, inline]

abbrev Lean.ConstMap : Type

Equations

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

structure Lean.Import : Type

• module : Name
• runtimeOnly : Bool

instance Lean.instReprImport : Repr Import

Equations

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

instance Lean.instInhabitedImport : Inhabited Import

Equations

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

instance Lean.instCoeNameImport : Coe Name Import

Equations

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

instance Lean.instToStringImport : ToString 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 : CompactedRegion → Bool

@[extern lean_compacted_region_free]

unsafe opaque Lean.CompactedRegion.free : 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 EnvExtensionEntry

structure Lean.ModuleData : Type

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

• imports : Array Import
• constNames : Array 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 ConstantInfo
• extraConstNames : Array 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 (Name × Array EnvExtensionEntry)

instance Lean.instInhabitedModuleData : Inhabited 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.

• mainModule : Name

  Name of the module being compiled.

• imports : Array Import

  Direct imports

• regions : Array CompactedRegion

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

• moduleNames : Array Name

  Name of all imported modules (directly and indirectly). The index of a module name in the array equals the ModuleIdx for the same module.

• moduleData : Array ModuleData

  Module data for all imported modules.

instance Lean.instNonemptyEnvironmentHeader : Nonempty EnvironmentHeader

structure Lean.Kernel.Diagnostics : Type

• unfoldCounter : PHashMap 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 Diagnostics

Equations

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

structure Lean.Kernel.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.

• constants : ConstMap

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

• 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. When the flag is set, the type checker can assume that the Quot declarations in the environment have indeed been added by the kernel and not by the user.

• diagnostics : Diagnostics

  Diagnostic information collected during kernel execution.

  Remark: We store kernel diagnostic information in an environment field 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.

• const2ModIdx : Std.HashMap Name 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.

• 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 : EnvironmentHeader

  The header contains additional information that is set at import time.

instance Lean.Kernel.instNonemptyEnvironment : Nonempty Environment

inductive Lean.Kernel.Exception : Type

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

• unknownConstant (env : Environment) (name : Name) : Exception
• alreadyDeclared (env : Environment) (name : Name) : Exception
• declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr) : Exception
• declHasMVars (env : Environment) (name : Name) (expr : Expr) : Exception
• declHasFVars (env : Environment) (name : Name) (expr : Expr) : Exception
• funExpected (env : Environment) (lctx : LocalContext) (expr : Expr) : Exception
• typeExpected (env : Environment) (lctx : LocalContext) (expr : Expr) : Exception
• letTypeMismatch (env : Environment) (lctx : LocalContext) (name : Name) (givenType expectedType : Expr) : Exception
• exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr expectedType : Expr) : Exception
• appTypeMismatch (env : Environment) (lctx : LocalContext) (app funType argType : Expr) : Exception
• invalidProj (env : Environment) (lctx : LocalContext) (proj : Expr) : Exception
• thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr) : Exception
• other (msg : String) : Exception
• deterministicTimeout : Exception
• excessiveMemory : Exception
• deepRecursion : Exception
• interrupted : Exception

@[export lean_environment_find]

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

Equations

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

@[extern lean_add_decl]

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

Type check given declaration and add it to the environment

@[extern lean_add_decl_without_checking]

opaque Lean.Kernel.Environment.addDeclWithoutChecking (env : Environment) (decl : Declaration) : Except Exception 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.

@[export lean_kernel_diag_is_enabled]

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

Equations

• Lean.Kernel.Environment.Diagnostics.isEnabled d = d.enabled

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

Enables/disables kernel diagnostics.

Equations

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

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

Equations

• env.isDiagnosticsEnabled = env.diagnostics.enabled

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

Equations

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

@[export lean_kernel_record_unfold]

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

Equations

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

@[export lean_kernel_get_diag]

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

Equations

• env.getDiagnostics = env.diagnostics

@[export lean_kernel_set_diag]

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

Equations

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

@[reducible, inline, deprecated Lean.Kernel.Exception (since := "2024-12-12")]

abbrev Lean.KernelException : Type

Equations

• Lean.KernelException = Lean.Kernel.Exception

inductive Lean.ConstantKind : Type

• defn : ConstantKind
• thm : ConstantKind
• axiom : ConstantKind
• opaque : ConstantKind
• quot : ConstantKind
• induct : ConstantKind
• ctor : ConstantKind
• recursor : ConstantKind

instance Lean.instInhabitedConstantKind : Inhabited ConstantKind

Equations

• Lean.instInhabitedConstantKind = { default := Lean.ConstantKind.defn }

instance Lean.instBEqConstantKind : BEq ConstantKind

Equations

• Lean.instBEqConstantKind = { beq := Lean.beqConstantKind✝ }

instance Lean.instReprConstantKind : Repr ConstantKind

Equations

• Lean.instReprConstantKind = { reprPrec := Lean.reprConstantKind✝ }

def Lean.ConstantKind.ofConstantInfo : ConstantInfo → ConstantKind

Equations

• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.defnInfo val) = Lean.ConstantKind.defn
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.thmInfo val) = Lean.ConstantKind.thm
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.axiomInfo val) = Lean.ConstantKind.axiom
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.opaqueInfo val) = Lean.ConstantKind.opaque
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.quotInfo val) = Lean.ConstantKind.quot
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.inductInfo val) = Lean.ConstantKind.induct
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.ctorInfo val) = Lean.ConstantKind.ctor
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.recInfo val) = Lean.ConstantKind.recursor

structure Lean.AsyncConstantInfo : Type

ConstantInfo variant that allows for asynchronous filling of components via tasks.

• name : Name

  The declaration name, known immediately.

• kind : ConstantKind

  The kind of the constant, known immediately.

• sig : Task ConstantVal

  The "signature" including level params and type, potentially filled asynchronously.

• constInfo : Task ConstantInfo

  The final, complete constant info, potentially filled asynchronously.

def Lean.AsyncConstantInfo.toConstantVal (c : AsyncConstantInfo) : ConstantVal

Equations

• c.toConstantVal = c.sig.get

def Lean.AsyncConstantInfo.toConstantInfo (c : AsyncConstantInfo) : ConstantInfo

Equations

• c.toConstantInfo = c.constInfo.get

def Lean.AsyncConstantInfo.ofConstantInfo (c : ConstantInfo) : AsyncConstantInfo

Equations

• Lean.AsyncConstantInfo.ofConstantInfo c = { name := c.name, kind := Lean.ConstantKind.ofConstantInfo c, sig := { get := c.toConstantVal }, constInfo := { get := c } }

structure Lean.AsyncContext : Type

Information about the current branch of the environment representing asynchronous elaboration.

• declPrefix : Name

  Name of the declaration asynchronous elaboration was started for. All constants added to this environment branch must have the name as a prefix, after erasing macro scopes and private name prefixes.

instance Lean.instNonemptyAsyncContext : Nonempty AsyncContext

def Lean.AsyncContext.mayContain (ctx : AsyncContext) (n : Name) : Bool

Checks whether a declaration named n may be added to the environment in the given context. See also AsyncContext.declPrefix.

Equations

• ctx.mayContain n = ctx.declPrefix.isPrefixOf (Lean.privateToUserName n.eraseMacroScopes)

structure Lean.AsyncConst : Type

Constant info and environment extension states eventually resulting from async elaboration.

• constInfo : AsyncConstantInfo
• exts? : Option (Task (Array EnvExtensionState))

  Reported extension state eventually fulfilled by promise; may be missing for tasks (e.g. kernel checking) that can eagerly guarantee they will not report any state.

structure Lean.AsyncConsts : Type

Data structure holding a sequence of AsyncConsts optimized for efficient access.

• toArray : Array AsyncConst
• map : Lean.NameMap Lean.AsyncConst

  Map from declaration name to const for fast direct access.

• normalizedTrie : Lean.NameTrie Lean.AsyncConst

  Trie of declaration names without private name prefixes for fast longest-prefix access.

instance Lean.instInhabitedAsyncConsts : Inhabited AsyncConsts

Equations

• Lean.instInhabitedAsyncConsts = { default := { toArray := default, map := default, normalizedTrie := default } }

def Lean.AsyncConsts.add (aconsts : AsyncConsts) (aconst : AsyncConst) : AsyncConsts

Equations

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

def Lean.AsyncConsts.find? (aconsts : AsyncConsts) (declName : Name) : Option AsyncConst

Equations

• aconsts.find? declName = (Lean.AsyncConsts.map✝ aconsts).find? declName

def Lean.AsyncConsts.findPrefix? (aconsts : AsyncConsts) (declName : Name) : Option AsyncConst

Finds the constant in the collection that is a prefix of declName, if any.

Equations

• aconsts.findPrefix? declName = (Lean.AsyncConsts.normalizedTrie✝ aconsts).findLongestPrefix? (Lean.privateToUserName declName.eraseMacroScopes)

structure Lean.Environment : Type

Elaboration-specific extension of Kernel.Environment that adds tracking of asynchronously elaborated declarations.

• checkedWithoutAsync : Kernel.Environment

  Kernel environment not containing any asynchronously elaborated declarations. Also stores environment extension state for the current branch of the environment.

  Ignoring extension state, this is guaranteed to be some prior version of checked that is eagerly available. Thus we prefer taking information from it instead of checked whenever possible.

• checked : Task Kernel.Environment

  Kernel environment task that is fulfilled when all asynchronously elaborated declarations are finished, containing the resulting environment. Also collects the environment extension state of all environment branches that contributed contained declarations.

• asyncConsts : Lean.AsyncConsts

  Container of asynchronously elaborated declarations, i.e. checked = checkedWithoutAsync ⨃ asyncConsts.

• asyncCtx? : Option Lean.AsyncContext

  Information about this asynchronous branch of the environment, if any.

instance Lean.instNonemptyEnvironment : Nonempty Environment

@[export lean_elab_environment_of_kernel_env]

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

Equations

• Lean.Environment.ofKernelEnv env = { checkedWithoutAsync := env, checked := { get := env }, asyncConsts := { toArray := #[], map := ∅, normalizedTrie := ∅ }, asyncCtx? := none }

@[export lean_elab_environment_to_kernel_env]

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

Equations

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

def Lean.Environment.asyncMayContain (env : Environment) (declName : Name) : Bool

Checks whether the given declaration name may potentially added, or have been added, to the current environment branch, which is the case either if this is the main branch or if the declaration name is a suffix (modulo privacy and hygiene information) of the top-level declaration name for which this branch was created.

This function should always be checked before modifying an AsyncMode.async environment extension to ensure findStateAsync will be able to find the modification from other branches.

Equations

• env.asyncMayContain declName = Option.all (fun (x : Lean.AsyncContext) => x.mayContain declName) (Lean.Environment.asyncCtx?✝ env)

def Lean.Environment.addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : Declaration) (cancelTk? : Option IO.CancelToken) (doCheck : Bool := true) : Except Kernel.Exception Environment

Adds given declaration to the environment, type checking it unless doCheck is false.

This is a plumbing function for the implementation of Lean.addDecl, most users should use it instead.

Equations

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

def Lean.Environment.constants (env : Environment) : ConstMap

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

Equations

• env.constants = env.toKernelEnv.constants

def Lean.Environment.const2ModIdx (env : Environment) : Std.HashMap Name 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.

Equations

• env.const2ModIdx = env.toKernelEnv.const2ModIdx

def Lean.Environment.addExtraName (env : Environment) (name : Name) : 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.

def Lean.Environment.findAsync? (env : Environment) (n : Name) : Option AsyncConstantInfo

Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration tasks.

Equations

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

def Lean.Environment.findConstVal? (env : Environment) (n : Name) : Option ConstantVal

Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration tasks for declaration bodies (which are not accessible from ConstantVal).

Equations

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

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

Looks up the given declaration name in the environment, blocking on the corresponding elaboration task if not yet complete.

Equations

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

def Lean.Environment.dbgFormatAsyncState (env : Environment) : BaseIO String

Returns debug output about the asynchronous state of the environment.

Equations

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

def Lean.Environment.dbgFormatCheckedSyncState (env : Environment) : BaseIO String

Returns debug output about the synchronous state of the environment.

Equations

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

structure Lean.Environment.AddConstAsyncResult : Type

Result of Lean.Environment.addConstAsync which is necessary to complete the asynchronous addition.

• mainEnv : Environment

  Resulting "main branch" environment which contains the declaration name as an asynchronous constant. Accessing the constant or kernel environment will block until the corresponding AddConstAsyncResult.commit* function has been called.

• asyncEnv : Environment

  Resulting "async branch" environment which should be used to add the desired declaration in a new task and then call AddConstAsyncResult.commit* to commit results back to the main environment. One of commitCheckEnv or commitFailure must be called eventually to prevent deadlocks on main branch accesses.

• constName : Lean.Name
• kind : Lean.ConstantKind
• sigPromise : IO.Promise Lean.ConstantVal
• infoPromise : IO.Promise Lean.ConstantInfo
• extensionsPromise : IO.Promise (Array Lean.EnvExtensionState)
• checkedEnvPromise : IO.Promise Lean.Kernel.Environment

def Lean.Environment.addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts : Bool := true) : IO AddConstAsyncResult

Starts the asynchronous addition of a constant to the environment. The environment is split into a "main" branch that holds a reference to the constant to be added but will block on access until the corresponding information has been added on the "async" environment branch and committed there; see the respective fields of AddConstAsyncResult as well as the [Environment Branches] note for more information.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitSignature (res : AddConstAsyncResult) (sig : ConstantVal) : IO Unit

Commits the signature of the constant to the main environment branch. The declaration name must match the name originally given to addConstAsync. It is optional to call this function but can help in unblocking corresponding accesses to the constant on the main branch.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment) (info? : Option ConstantInfo := none) : IO Unit

Commits the full constant info to the main environment branch. If info? is none, it is taken from the given environment. The declaration name and kind must match the original values given to addConstAsync. The signature must match the previous commitSignature call, if any.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitFailure (res : AddConstAsyncResult) : BaseIO Unit

Aborts async addition, filling in missing information with default values/sorries and leaving the kernel environment unchanged.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Environment) : IO Unit

Assuming Lean.addDecl has been run for the constant to be added on the async environment branch, commits the full constant info from that call to the main environment, waits for the final kernel environment resulting from the addDecl call, and commits it to the main branch as well, unblocking kernel additions there. All commitConst preconditions apply.

Equations

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

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

Equations

• env.contains n = (env.findAsync? n).isSome

def Lean.Environment.header (env : Environment) : EnvironmentHeader

Equations

• env.header = env.checkedWithoutAsync.header

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

Equations

• env.imports = env.header.imports

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

Equations

• env.allImportedModuleNames = env.header.moduleNames

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

Equations

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

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

Equations

• env.mainModule = env.header.mainModule

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

inductive Lean.EnvExtension.AsyncMode : Type

Async access mode for environment extensions used in EnvironmentExtension.get/set/modifyState. Depending on their specific uses, extensions may opt out of the strict sync access mode in order to avoid blocking parallel elaboration and/or to optimize accesses. The access mode is set at environment extension registration time but can be overriden at EnvironmentExtension.getState in order to weaken it for specific accesses.

In all modes, the state stored into the .olean file for persistent environment extensions is the result of getState called on the main environment branch at the end of the file, i.e. it encompasses all modifications for all modes but local.

• sync : AsyncMode

  Default access mode, writing and reading the extension state to/from the full checked environment. This mode ensures the observed state is identical independently of whether or how parallel elaboration is used but getState will block on all prior environment branches by waiting for checked. setState and modifyState do not block.

  While a safe default, any extension that reasonably could be used in parallel elaboration contexts should opt for a weaker mode to avoid blocking unless there is no way to access the correct state without waiting for all prior environment branches, in which case its data management should be restructured if at all possible.

• local : AsyncMode

  Accesses only the state of the current environment branch. Modifications on other branches are not visible and are ultimately discarded except for the main branch. Provides the fastest accessors, will never block.

  This mode is particularly suitable for extensions where state does not escape from lexical scopes even without parallelism, e.g. ScopedEnvExtensions when setting local entries.

• mainOnly : AsyncMode

  Like local but panics when trying to modify the state on anything but the main environment branch. For extensions that fulfill this requirement, all modes functionally coincide but this is the safest and most efficient choice in that case, preventing accidental misuse.

  This mode is suitable for extensions that are modified only at the command elaboration level before any environment forks in the command, and in particular for extensions that are modified only at the very beginning of the file.

• async : AsyncMode

  Accumulates modifications in the checked environment like sync, but getState will panic instead of blocking. Instead findStateAsync should be used, which will access the state of the environment branch corresponding to the passed declaration name, if any, or otherwise the state of the current branch. In other words, at most one environment branch will be blocked on instead of all prior branches. The local state can still be accessed by calling getState with mode local explicitly.

  This mode is suitable for extensions with map-like state where the key uniquely identifies the top-level declaration where it could have been set, e.g. because the key on modification is always the surrounding declaration's name. Any calls to modifyState/setState should assert asyncMayContain with that key to ensure state is never accidentally stored in a branch where it cannot be found by findStateAsync. In particular, this mode is closest to how the environment's own constant map works which asserts the same predicate on modification and provides findAsync? for block-avoiding access.

instance Lean.EnvExtension.instInhabitedAsyncMode : Inhabited AsyncMode

Equations

• Lean.EnvExtension.instInhabitedAsyncMode = { default := Lean.EnvExtension.AsyncMode.sync }

structure Lean.EnvExtension (σ : Type) : Type

Environment extension, can only be generated by registerEnvExtension that allocates a unique index for this extension into each environment's extension state's array.

• idx : Nat
• mkInitial : IO σ
• asyncMode : AsyncMode

instance Lean.instInhabitedEnvExtension {a✝ : Type} : Inhabited (EnvExtension a✝)

Equations

• Lean.instInhabitedEnvExtension = { default := { idx := default, mkInitial := default, asyncMode := default } }

def Lean.EnvExtension.ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Array 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.EnvExtension.ensureExtensionsArraySize exts = Lean.EnvExtension.ensureExtensionsArraySize.loop exts.size exts

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

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

Equations

• Lean.EnvExtension.mkInitialExtStates = do let exts ← ST.Ref.get Lean.EnvExtension.envExtensionsRef✝ Array.mapM (fun (ext : Lean.EnvExtension Lean.EnvExtensionState) => ext.mkInitial) exts

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

Applies the given function to the extension state. See AsyncMode for details on how modifications from different environment branches are reconciled.

Note that in modes sync and async, f will be called twice, on the local and on the checked state.

Equations

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

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

Sets the extension state to the given value. See AsyncMode for details on how modifications from different environment branches are reconciled.

Equations

• ext.setState env s = inline (ext.modifyState env fun (x : σ) => s)

@[implemented_by _private.Lean.Environment.0.Lean.EnvExtension.getStateUnsafe]

opaque Lean.EnvExtension.getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) (asyncMode : AsyncMode := ext.asyncMode) : σ

Returns the current extension state. See AsyncMode for details on how modifications from different environment branches are reconciled. Panics if the extension is marked as async; see its documentation for more details. Overriding the extension's default AsyncMode is usually not recommended and should be considered only for important optimizations.

def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.mainOnly) : IO (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

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

@[export lean_mk_empty_environment]

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

Equations

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

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

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

structure Lean.ImportM.Context : Type

• env : Environment
• opts : Options

@[reducible, inline]

abbrev Lean.ImportM (α : Type) : Type

Equations

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

structure Lean.PersistentEnvExtension (α β σ : 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 : EnvExtension (PersistentEnvExtensionState α σ)
• name : Name
• addImportedFn : Array (Array α) → ImportM σ
• addEntryFn : σ → β → σ
• exportEntriesFn : σ → Array α
• statsFn : σ → Format

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

Equations

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

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

Equations

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

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

Equations

• ext.getModuleEntries env m = (ext.toEnvExtension.getState env Lean.EnvExtension.AsyncMode.local).importedEntries.get! m

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

Equations

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

def Lean.PersistentEnvExtension.getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : 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} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : 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} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) : 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 }

@[implemented_by _private.Lean.Environment.0.Lean.PersistentEnvExtension.findStateAsyncUnsafe]

opaque Lean.PersistentEnvExtension.findStateAsync {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) (declPrefix : Name) : σ

Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

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

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

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

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

Equations

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

@[implemented_by Lean.registerPersistentEnvExtensionUnsafe]

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

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

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

Equations

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

@[specialize #[]]

def Lean.mkStateFromImportedEntries {α σ : 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

• name : Name
• addEntryFn : σ → α → σ
• addImportedFn : Array (Array α) → σ
• toArrayFn : List α → Array α
• asyncMode : EnvExtension.AsyncMode

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

Equations

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

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

Equations

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

def Lean.SimplePersistentEnvExtension.getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : 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} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) : σ

Get the current state of the given SimplePersistentEnvExtension.

Equations

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

def Lean.SimplePersistentEnvExtension.setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) : 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} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) : 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 Lean.Name Lean.NameSet

def Lean.mkTagDeclarationExtension (name : Name := by exact decl_name%) : IO TagDeclarationExtension

Equations

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

instance Lean.TagDeclarationExtension.instInhabited : Inhabited TagDeclarationExtension

Equations

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

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

Equations

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

def Lean.TagDeclarationExtension.isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : 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.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)

def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[extern lean_save_module_data]

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

@[extern lean_read_module_data]

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

@[noinline, export lean_environment_free_regions]

unsafe def Lean.Environment.freeRegions (env : 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.

Equations

• env.freeRegions = Array.forM Lean.CompactedRegion.free env.header.regions

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

Equations

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

@[export lean_write_module]

def Lean.writeModule (env : Environment) (fname : System.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 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 : Environment → IO 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 : NameHashSet
• moduleNames : Array Name
• moduleData : Array ModuleData
• regions : Array CompactedRegion

def Lean.throwAlreadyImported {α : Type} (s : ImportState) (const2ModIdx : Std.HashMap Name ModuleIdx) (modIdx : Nat) (cname : 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 : ImportStateM α) (s : ImportState := { moduleNameSet := ∅, moduleNames := #[], moduleData := #[], regions := #[] }) : IO (α × ImportState)

Equations

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

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

def Lean.finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (leakEnv : Bool := false) : IO 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 Import) (opts : Options) (trustLevel : UInt32 := 0) (leakEnv : Bool := false) : IO Environment

Equations

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

unsafe def Lean.withImportModules {α : Type} (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (act : 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.

Equations

• Lean.withImportModules imports opts trustLevel act = do let env ← Lean.importModules imports opts trustLevel tryFinally (act env) env.freeRegions

opaque Lean.namespacesExt : SimplePersistentEnvExtension Name NameSSet

Environment extension for tracking all namespace declared by users.

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

Enables/disables kernel diagnostics.

Equations

• Lean.Kernel.enableDiag env flag = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.enableDiag flag

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

Equations

• Lean.Kernel.isDiagnosticsEnabled env = env.checkedWithoutAsync.isDiagnosticsEnabled

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

Equations

• Lean.Kernel.resetDiag env = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.resetDiag

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

Equations

• Lean.Kernel.getDiagnostics env = env.checked.get.diagnostics

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

Equations

• Lean.Kernel.setDiagnostics env diag = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.setDiagnostics diag

def Lean.Environment.registerNamespace (env : Environment) (n : Name) : 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 : Environment) (n : 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 : Environment) : 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 : 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 : Environment) (opts : Options) (constName : 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 : Environment) (opts : Options) (typeName constName : 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 α.

Equations

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

def Lean.Environment.hasUnsafe (env : Environment) (e : 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 : LocalContext) (a b : Expr) : Except Exception 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 : LocalContext) (a b : 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 : LocalContext) (a : Expr) : Except Exception 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 : LocalContext) (a : Expr) : Except Exception 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 Environment
• modifyEnv : (Environment → Environment) → m Unit

@[always_inline]

instance Lean.instMonadEnvOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadEnv m] : 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] [MonadEnv m] (name : Name) (levelParams : List Name) (type value : Expr) (hints : ReducibilityHints) : m DefinitionVal

Constructs a DefinitionVal, inferring the unsafe field

Equations

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