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

• global: {α : Type} → α → Lean.ScopedEnvExtension.Entry α
• scoped: {α : Type} → Lean.Name → α → Lean.ScopedEnvExtension.Entry α

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

• state : σ
• activeScopes : Lean.NameSet

Instances For

• instInhabitedState_mathlib

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

• map : Lean.SMap Lean.Name (Lean.PArray β)

Instances For

• Lean.ScopedEnvExtension.instInhabitedScopedEntries

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

Equations

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

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

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

Instances For

• Lean.ScopedEnvExtension.instInhabitedStateStack

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

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

• name : Lean.Name
• mkInitial : IO σ
• ofOLeanEntry : σ → α → Lean.ImportM β
• toOLeanEntry : β → α
• addEntry : σ → β → σ
• finalizeImport : σ → σ

Instances For

• Lean.ScopedEnvExtension.instInhabitedDescr

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

• Lean.ScopedEnvExtension.exportEntriesFn s = s.newEntries.toArray.reverse

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

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

Instances For

• Lean.instInhabitedScopedEnvExtension

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

Equations

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

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

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

@[implemented_by Lean.registerScopedEnvExtensionUnsafe]

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

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

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

Equations

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

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

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

Equations

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

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

def Lean.ScopedEnvExtension.addCore {α β σ : Type} (env : Lean.Environment) (ext : Lean.ScopedEnvExtension α β σ) (b : β) (kind : Lean.AttributeKind) (namespaceName : Lean.Name) : Lean.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] [Lean.MonadResolveName m] [Lean.MonadEnv m] (ext : Lean.ScopedEnvExtension α β σ) (b : β) (kind : Lean.AttributeKind := Lean.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 : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) : σ

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

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

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

def Lean.popScope {m : Type → Type} [Monad m] [Lean.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] [Lean.MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (namespaceName : Lean.Name) : m Unit

Equations

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

@[reducible, inline]

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

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

• name : Lean.Name
• addEntry : σ → α → σ
• initial : σ
• finalizeImport : σ → σ

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

Equations

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