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

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

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

• state : σ
• activeScopes : Lean.NameSet

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

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

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

Equations

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

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

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

instance Lean.ScopedEnvExtension.instInhabitedStateStack : {a a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension.StateStack a a_1 a_2)

Equations

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

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

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

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

Equations

• Lean.ScopedEnvExtension.instInhabitedDescr = { default := Lean.ScopedEnvExtension.Descr.mk default default default (fun (s : σ) (x : β) => s) id }

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.ScopedEnvExtension.addEntryFn {α : Type} {β : Type} {σ : 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} {β : Type} {σ : Type} (s : Lean.ScopedEnvExtension.StateStack α β σ) : Array (Lean.ScopedEnvExtension.Entry α)

Equations

• Lean.ScopedEnvExtension.exportEntriesFn s = Array.reverse (List.toArray s.newEntries)

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

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

instance Lean.instInhabitedScopedEnvExtension : {a : Type} → [inst : Inhabited a] → {a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension a a_1 a_2)

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} {β : Type} {σ : Type} (descr : Lean.ScopedEnvExtension.Descr α β σ) : IO (Lean.ScopedEnvExtension α β σ)

Equations

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

@[implemented_by Lean.registerScopedEnvExtensionUnsafe]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.pushScope {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.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 : Lake.Name) : m Unit

Equations

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

@[inline, reducible]

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

Equations

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

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

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

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

Equations

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