inductive Lean.ScopedEnvExtension.Entry (α : Type) : Type

• global {α : Type} : α → Entry α
• scoped {α : Type} : Name → α → Entry α

structure Lean.ScopedEnvExtension.State (σ : Type) : Type

• state : σ
• activeScopes : NameSet
• delimitsLocal : Bool

structure Lean.ScopedEnvExtension.ScopedEntries (β : Type) : Type

• map : SMap Name (PArray β)

@[implicit_reducible]

instance Lean.ScopedEnvExtension.instInhabitedScopedEntries {a✝ : Type} : Inhabited (ScopedEntries a✝)

def Lean.ScopedEnvExtension.instInhabitedScopedEntries.default {a✝ : Type} : ScopedEntries a✝

structure Lean.ScopedEnvExtension.StateStack (α β σ : Type) : Type

• stateStack : List (State σ)
• scopedEntries : ScopedEntries β
• newEntries : List (Entry α)

def Lean.ScopedEnvExtension.instInhabitedStateStack.default {a✝ a✝¹ a✝² : Type} : StateStack a✝ a✝¹ a✝²

@[implicit_reducible]

instance Lean.ScopedEnvExtension.instInhabitedStateStack {a✝ a✝¹ a✝² : Type} : Inhabited (StateStack a✝ a✝¹ a✝²)

structure Lean.ScopedEnvExtension.Descr (α β σ : Type) : Type

• name : Name
• mkInitial : IO σ
• ofOLeanEntry : σ → α → ImportM β
• toOLeanEntry : β → α
• addEntry : σ → β → σ
• finalizeImport : σ → σ
• exportEntry? : OLeanLevel → α → Option α

@[implicit_reducible]

instance Lean.ScopedEnvExtension.instInhabitedDescr {α β σ : Type} [Inhabited α] : Inhabited (Descr α β σ)

def Lean.ScopedEnvExtension.mkInitial {α β σ : Type} (descr : Descr α β σ) : IO (StateStack α β σ)

def Lean.ScopedEnvExtension.ScopedEntries.insert {β : Type} (scopedEntries : ScopedEntries β) (ns : Name) (b : β) : ScopedEntries β

def Lean.ScopedEnvExtension.addImportedFn {α β σ : Type} (descr : Descr α β σ) (as : Array (Array (Entry α))) : ImportM (StateStack α β σ)

def Lean.ScopedEnvExtension.addEntryFn {α β σ : Type} (descr : Descr α β σ) (s : StateStack α β σ) (e : Entry β) : StateStack α β σ

def Lean.ScopedEnvExtension.exportEntriesFn {α β σ : Type} (descr : Descr α β σ) (level : OLeanLevel) (s : StateStack α β σ) : Array (Entry α)

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

• descr : Descr α β σ
• ext : PersistentEnvExtension (Entry α) (Entry β) (StateStack α β σ)

def Lean.instInhabitedScopedEnvExtension.default {a✝ : Type} [Inhabited a✝] {a✝¹ a✝² : Type} : ScopedEnvExtension a✝ a✝¹ a✝²

@[implicit_reducible]

instance Lean.instInhabitedScopedEnvExtension {a✝ : Type} [Inhabited a✝] {a✝¹ a✝² : Type} : Inhabited (ScopedEnvExtension a✝ a✝¹ a✝²)

opaque Lean.scopedEnvExtensionsRef : IO.Ref (Array (ScopedEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState))

unsafe def Lean.registerScopedEnvExtensionUnsafe {α β σ : Type} (descr : ScopedEnvExtension.Descr α β σ) : IO (ScopedEnvExtension α β σ)

@[implemented_by Lean.registerScopedEnvExtensionUnsafe]

opaque Lean.registerScopedEnvExtension {α β σ : Type} (descr : ScopedEnvExtension.Descr α β σ) : IO (ScopedEnvExtension α β σ)

def Lean.ScopedEnvExtension.pushScope {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment

def Lean.ScopedEnvExtension.popScope {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment

def Lean.ScopedEnvExtension.setDelimitsLocal {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment

Modifies delimitsLocal flag to false to turn off delimiting of local entries.

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

def Lean.ScopedEnvExtension.addScopedEntry {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) (b : β) : Environment

def Lean.stateStackModify {α β σ : Type} (ext : ScopedEnvExtension α β σ) (states : List (ScopedEnvExtension.State σ)) (b : β) : List (ScopedEnvExtension.State σ)

The following function is used to implement end_local_scope command.

By default, all states have delimitsLocal set to true, and the following code modifies only the top element of the stack. If the top element’s delimitsLocal is false, the function instead traverses down the stack until it reaches the first state where delimitsLocal is true. Intuitively, delimitsLocal of each State determines whether local entries are delimited. When set to false, it allows traversal through implicit scopes where local entries are not delimited.

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

def Lean.ScopedEnvExtension.addCore {α β σ : Type} (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment

def Lean.ScopedEnvExtension.add {m : Type → Type} {α β σ : Type} [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind := AttributeKind.global) : m Unit

def Lean.ScopedEnvExtension.getState {σ α β : Type} [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) (asyncMode : EnvExtension.AsyncMode := ext.ext.toEnvExtension.asyncMode) : σ

def Lean.ScopedEnvExtension.activateScoped {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) : Environment

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

def Lean.pushScope {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit

def Lean.popScope {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit

def Lean.setDelimitsLocal {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit

Used to implement end_local_scope command, that disables delimiting local entries of ScopedEnvExtension in a current scope.

def Lean.activateScoped {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (namespaceName : Name) : m Unit

@[reducible, inline]

abbrev Lean.SimpleScopedEnvExtension (α σ : Type) : Type

structure Lean.SimpleScopedEnvExtension.Descr (α σ : Type) : Type

• name : Name
• addEntry : σ → α → σ
• initial : σ
• finalizeImport : σ → σ
• exportEntry? : OLeanLevel → α → Option α

def Lean.registerSimpleScopedEnvExtension {α σ : Type} (descr : SimpleScopedEnvExtension.Descr α σ) : IO (SimpleScopedEnvExtension α σ)