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✝)

Equations

• Lean.ScopedEnvExtension.instInhabitedScopedEntries = { default := { map := default } }

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✝²)

Equations

• Lean.ScopedEnvExtension.instInhabitedStateStack = { default := { stateStack := default, scopedEntries := default, newEntries := default } }

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

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

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

Equations

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

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

Equations

• Lean.ScopedEnvExtension.mkInitial descr = do let __do_lift ← descr.mkInitial pure { stateStack := [{ state := __do_lift }] }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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✝²)

Equations

• Lean.instInhabitedScopedEnvExtension = { default := { descr := default, ext := default } }

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

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

Equations

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

@[implemented_by Lean.registerScopedEnvExtensionUnsafe]

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

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

Equations

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

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

Equations

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

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

Equations

• ext.addEntry env b = ext.ext.addEntry env (Lean.ScopedEnvExtension.Entry.global b)

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

Equations

• ext.addScopedEntry env namespaceName b = ext.ext.addEntry env (Lean.ScopedEnvExtension.Entry.scoped namespaceName b)

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

Equations

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

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

Equations

• Lean.ScopedEnvExtension.addCore env ext b Lean.AttributeKind.global namespaceName = ext.addEntry env b
• Lean.ScopedEnvExtension.addCore env ext b Lean.AttributeKind.local namespaceName = ext.addLocalEntry env b
• Lean.ScopedEnvExtension.addCore env ext b Lean.AttributeKind.scoped namespaceName = ext.addScopedEntry env namespaceName b

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

Equations

• ext.add b kind = do let ns ← Lean.getCurrNamespace Lean.modifyEnv fun (x : Lean.Environment) => Lean.ScopedEnvExtension.addCore x ext b kind ns

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.SimpleScopedEnvExtension α σ = Lean.ScopedEnvExtension α α σ

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

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

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

Equations

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