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

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

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

• state : σ
• activeScopes : NameSet

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

• map : SMap Name (PArray β)

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

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

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

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 : σ → σ

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} (s : StateStack α β σ) : Array (Entry α)

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

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

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.addEntry {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment

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

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.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 : σ → σ

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