Lean.Environment

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

source

@[extern lean_compacted_region_is_memory_mapped]

opaque Lean.CompactedRegion.isMemoryMapped:

Lean.CompactedRegion → Bool

source

@[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.

source

opaque Lean.EnvExtensionEntrySpec:

NonemptyType

source

def Lean.EnvExtensionEntry:

Type

Equations

Lean.EnvExtensionEntry = NonemptyType.type Lean.EnvExtensionEntrySpec

source

instance Lean.instNonemptyEnvExtensionEntry:

Nonempty Lean.EnvExtensionEntry

Equations

Lean.instNonemptyEnvExtensionEntry = Lean.instNonemptyEnvExtensionEntry.proof_1

source

structure Lean.ModuleData:

Type

imports : Array Lean.Import
constants : Array Lean.ConstantInfo
entries : Array (Lean.Name × Array Lean.EnvExtensionEntry)

source

instance Lean.instInhabitedModuleData:

Inhabited Lean.ModuleData

Equations

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

source

structure Lean.EnvironmentHeader:

Type

trustLevel : UInt32
quotInit : Bool
mainModule : Lean.Name
imports : Array Lean.Import
regions : Array Lean.CompactedRegion
moduleNames : Array Lean.Name
moduleData : Array Lean.ModuleData

source

instance Lean.instInhabitedEnvironmentHeader:

Inhabited Lean.EnvironmentHeader

Equations

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

source

structure Lean.Environment:

Type

const2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx
constants : Lean.ConstMap
extensions : Array Lean.EnvExtensionState
header : Lean.EnvironmentHeader

source

instance Lean.instInhabitedEnvironment:

Inhabited Lean.Environment

Equations

Lean.instInhabitedEnvironment = { default := { const2ModIdx := default, constants := default, extensions := default, header := default } }

source

def Lean.Environment.addAux (env : Lean.Environment) (cinfo : Lean.ConstantInfo) :

Lean.Environment

Equations

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

source

@[export lean_environment_find]

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

Option Lean.ConstantInfo

Equations

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

source

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

Bool

Equations

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

source

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

Array Lean.Import

Equations

Lean.Environment.imports env = env.header.imports

source

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

Array Lean.Name

Equations

Lean.Environment.allImportedModuleNames env = env.header.moduleNames

source

@[export lean_environment_set_main_module]

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

Lean.Environment

Equations

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

source

@[export lean_environment_main_module]

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

Lean.Name

Equations

Lean.Environment.mainModule env = env.header.mainModule

source

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

Option Lean.ModuleIdx

Equations

Lean.Environment.getModuleIdxFor? env declName = Std.HashMap.find? env.const2ModIdx declName

source

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

Bool

Equations

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

source

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

Option Lean.ModuleIdx

Equations

Lean.Environment.getModuleIdx? env moduleName = Array.findIdx? env.header.moduleNames fun a => a == moduleName

source

inductive Lean.KernelException:

Type

unknownConstant: Lean.Environment → Lean.Name → Lean.KernelException
alreadyDeclared: Lean.Environment → Lean.Name → Lean.KernelException
declTypeMismatch: Lean.Environment → Lean.Declaration → Lean.Expr → Lean.KernelException
declHasMVars: Lean.Environment → Lean.Name → Lean.Expr → Lean.KernelException
declHasFVars: Lean.Environment → Lean.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 → Lean.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
other: String → Lean.KernelException

source

@[extern lean_add_decl]

opaque Lean.Environment.addDecl (env : Lean.Environment) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

source

@[extern lean_compile_decl]

opaque Lean.Environment.compileDecl (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

source

def Lean.Environment.addAndCompile (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) :

Except Lean.KernelException Lean.Environment

Equations

Lean.Environment.addAndCompile env opt decl = do let env ← Lean.Environment.addDecl env decl Lean.Environment.compileDecl env opt decl

source

structure Lean.EnvExtensionInterface:

Type 1

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

source

instance Lean.instInhabitedEnvExtensionInterface:

Inhabited Lean.EnvExtensionInterface

Equations

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

source

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

Type

idx : Nat
mkInitial : IO σ

source

instance Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt:

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

Equations

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

source

def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize (env : Lean.Environment) :

IO Lean.Environment

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 env = Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop (Array.size env.extensions) env

source

partial def Lean.EnvExtensionInterfaceUnsafe.ensureExtensionsArraySize.loop (i : Nat) (env : Lean.Environment) :

IO Lean.Environment

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.setState {σ : Type} (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (env : Lean.Environment) (s : σ) :

Lean.Environment

Equations

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

source

@[inline]

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

Lean.Environment

Equations

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

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.getState {σ : Type} [inst : Inhabited σ] (ext : Lean.EnvExtensionInterfaceUnsafe.Ext σ) (env : Lean.Environment) :

Equations

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

source

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

IO (Lean.EnvExtensionInterfaceUnsafe.Ext σ)

Equations

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

source

def Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates:

IO (Array Lean.EnvExtensionState)

Equations

Lean.EnvExtensionInterfaceUnsafe.mkInitialExtStates = do let exts ← ST.Ref.get Lean.EnvExtensionInterfaceUnsafe.envExtensionsRef Array.mapM (fun ext => ext.mkInitial) exts

source

unsafe def Lean.EnvExtensionInterfaceUnsafe.imp:

Lean.EnvExtensionInterface

Equations

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

source

@[implementedBy Lean.EnvExtensionInterfaceUnsafe.imp]

opaque Lean.EnvExtensionInterfaceImp:

Lean.EnvExtensionInterface

source

def Lean.EnvExtension (σ : Type) :

Type

Equations

Lean.EnvExtension σ = Lean.EnvExtensionInterface.ext Lean.EnvExtensionInterfaceImp σ

source

instance Lean.EnvExtension.instInhabitedEnvExtension {σ : Type} [s : Inhabited σ] :

Inhabited (Lean.EnvExtension σ)

Equations

Lean.EnvExtension.instInhabitedEnvExtension = Lean.EnvExtensionInterface.inhabitedExt Lean.EnvExtensionInterfaceImp s

source

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

Lean.Environment

Equations

Lean.EnvExtension.setState ext env s = Lean.EnvExtensionInterface.setState Lean.EnvExtensionInterfaceImp ext env s

source

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

Lean.Environment

Equations

Lean.EnvExtension.modifyState ext env f = Lean.EnvExtensionInterface.modifyState Lean.EnvExtensionInterfaceImp ext env f

source

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

Equations

Lean.EnvExtension.getState ext env = Lean.EnvExtensionInterface.getState Lean.EnvExtensionInterfaceImp ext env

source

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

IO (Lean.EnvExtension σ)

Equations

Lean.registerEnvExtension mkInitial = Lean.EnvExtensionInterface.registerExt Lean.EnvExtensionInterfaceImp mkInitial

source

@[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.

source

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

Type

importedEntries : Array (Array α)
state : σ

source

structure Lean.ImportM.Context:

Type

env : Lean.Environment
opts : Lean.Options

source

@[inline]

abbrev Lean.ImportM (α : Type) :

Type

Equations

Lean.ImportM = ReaderT Lean.ImportM.Context IO

source

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

Type

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

source

instance Lean.instInhabitedPersistentEnvExtensionState {α : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.PersistentEnvExtensionState α σ)

Equations

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

source

instance Lean.instInhabitedPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.PersistentEnvExtension α β σ)

Equations

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

source

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

Array α

Equations

Lean.PersistentEnvExtension.getModuleEntries ext env m = Array.get! (Lean.EnvExtension.getState ext.toEnvExtension env).importedEntries m

source

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.

source

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

Equations

Lean.PersistentEnvExtension.getState ext env = (Lean.EnvExtension.getState ext.toEnvExtension env).state

source

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

Lean.Environment

Equations

Lean.PersistentEnvExtension.setState ext env s = Lean.EnvExtension.modifyState ext.toEnvExtension env fun ps => { importedEntries := ps.importedEntries, state := s }

source

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

Lean.Environment

Equations

Lean.PersistentEnvExtension.modifyState ext env f = Lean.EnvExtension.modifyState ext.toEnvExtension env fun ps => { importedEntries := ps.importedEntries, state := f ps.state }

source

opaque Lean.persistentEnvExtensionsRef:

IO.Ref (Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))

source

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

Type

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

source

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

IO (Lean.PersistentEnvExtension α β σ)

Equations

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

source

@[implementedBy Lean.registerPersistentEnvExtensionUnsafe]

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

IO (Lean.PersistentEnvExtension α β σ)

source

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

Type

Equations

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

source

@[specialize]

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

Equations

Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun r es => Array.foldl (fun r e => addEntryFn r e) r es 0 (Array.size es)) initState as 0 (Array.size as)

source

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

Type

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

source

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

IO (Lean.SimplePersistentEnvExtension α σ)

Equations

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

source

instance Lean.SimplePersistentEnvExtension.instInhabitedSimplePersistentEnvExtension {α : Type} {σ : Type} [inst : Inhabited σ] :

Inhabited (Lean.SimplePersistentEnvExtension α σ)

Equations

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

source

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

List α

Equations

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

source

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

Equations

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

source

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

Lean.Environment

Equations

Lean.SimplePersistentEnvExtension.setState ext env s = Lean.PersistentEnvExtension.modifyState ext env fun x => match x with | (entries, snd) => (entries, s)

source

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

Lean.Environment

Equations

Lean.SimplePersistentEnvExtension.modifyState ext env f = Lean.PersistentEnvExtension.modifyState ext env fun x => match x with | (entries, s) => (entries, f s)

source

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

source

def Lean.mkTagDeclarationExtension (name : Lean.Name) :

IO Lean.TagDeclarationExtension

Equations

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

source

instance Lean.TagDeclarationExtension.instInhabitedTagDeclarationExtension:

Inhabited Lean.TagDeclarationExtension

Equations

Lean.TagDeclarationExtension.instInhabitedTagDeclarationExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet))

source

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

Lean.Environment

Equations

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

source

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

Bool

Equations

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

source

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 (Lean.Name × α) (Lean.NameMap α)

source

def Lean.mkMapDeclarationExtension {α : Type} [inst : Inhabited α] (name : Lean.Name) :

IO (Lean.MapDeclarationExtension α)

Equations

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

source

instance Lean.MapDeclarationExtension.instInhabitedMapDeclarationExtension {α : Type} :

Inhabited (Lean.MapDeclarationExtension α)

Equations

Lean.MapDeclarationExtension.instInhabitedMapDeclarationExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)))

source

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

Lean.Environment

Equations

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

source

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

Option α

Equations

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

source

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

Bool

Equations

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

source

@[extern lean_save_module_data]

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

IO Unit

source

@[extern lean_read_module_data]

opaque Lean.readModuleData (fname : System.FilePath) :

IO (Lean.ModuleData × Lean.CompactedRegion)

source

@[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.

Equations

Lean.Environment.freeRegions env = Array.forM Lean.CompactedRegion.free env.header.regions 0 (Array.size env.header.regions)

source

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

IO Lean.ModuleData

Equations

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

source

@[export lean_write_module]

def Lean.writeModule (env : Lean.Environment) (fname : System.FilePath) :

IO Unit

Equations

Lean.writeModule env fname = do let a ← Lean.mkModuleData env Lean.saveModuleData fname (Lean.Environment.mainModule env) a

source

@[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.

source

@[extern 1 lean_get_num_attributes]

opaque Lean.getNumBuiltiAttributes:

IO Nat

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

source

structure Lean.ImportState:

Type

moduleNameSet : Lean.NameSet
moduleNames : Array Lean.Name
moduleData : Array Lean.ModuleData
regions : Array Lean.CompactedRegion

source

@[export lean_import_modules]

def Lean.importModules (imports : List Lean.Import) (opts : Lean.Options) (trustLevel : optParam UInt32 0) :

IO Lean.Environment

Equations

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

source

partial def Lean.importModules.importMods:

List Lean.Import → StateRefT' IO.RealWorld Lean.ImportState IO Unit

source

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

Equations

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

source

opaque Lean.namespacesExt:

Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSSet

source

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

Lean.Environment

Equations

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

source

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

Bool

Equations

Lean.Environment.isNamespace env n = Lean.NameSSet.contains (Lean.SimplePersistentEnvExtension.getState Lean.namespacesExt env) n

source

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

Lean.NameSSet

Equations

Lean.Environment.getNamespaceSet env = Lean.SimplePersistentEnvExtension.getState Lean.namespacesExt env

source

@[export lean_environment_add]

def Lean.Environment.add (env : Lean.Environment) (cinfo : Lean.ConstantInfo) :

Lean.Environment

Equations

Lean.Environment.add env cinfo = let env := Lean.Environment.registerNamePrefixes env (Lean.ConstantInfo.name cinfo); Lean.Environment.addAux env cinfo

source

@[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.

source

@[extern lean_eval_const]

unsafe opaque Lean.Environment.evalConst (α : Type u_1) (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.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.

source

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

source

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

Bool

Equations

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

source

@[extern lean_kernel_is_def_eq]

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

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.

source

@[extern lean_kernel_whnf]

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

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.

source

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

Type

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

Instances

source

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

Lean.MonadEnv n

Equations

Lean.instMonadEnv m n = { getEnv := liftM Lean.getEnv, modifyEnv := fun f => liftM (Lean.modifyEnv f) }