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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.ScopedEnvExtension.instInhabitedStateStack = { default := Lean.ScopedEnvExtension.instInhabitedStateStack.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 α β σ)

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

Equations

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

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

Equations

• Lean.instInhabitedScopedEnvExtension = { default := Lean.instInhabitedScopedEnvExtension.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.setDelimitsLocal {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment

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

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.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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.stateStackModify ext [] 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.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.

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.