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

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

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

• state : σ
• activeScopes : NameSet
• delimitsLocal : Bool
• scopeChanged : Bool

  Whether this state may differ from the enclosing scope's state because of changes made since this scope was pushed: local entries, entries of namespaces activated in this scope, and ScopedEnvExtension.modifyState. Popping a scope with this flag set bumps the generation to a fresh value (see PersistentEnvExtensionDescrCore.trackGen) and, for an extension with logWrites, logs scopeChangedDecls. Only tracked for extensions with Descr.tracksScopes.

• scopeChangedDecls : Array Name

  The declarations of the entries added since this scope was pushed, which popping it removes again; collected only for extensions with Descr.entryDecl?.

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

• map : SMap Name (PArray β)

@[instance_reducible]

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

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

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

@[instance_reducible]

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 : σ → σ
• exportEntry? : Environment → α → OLeanEntries (Option α)
• trackGen : Bool

  See PersistentEnvExtensionDescrCore.trackGen.

• logWrites : Bool

  See EnvExtension.logWrites.

• entryDecl? : Option (β → Name)

  The declaration an entry is about. Required with logWrites: adding an entry and scope operations adding or removing entries log their declarations (Environment.logDeclChange).

def Lean.ScopedEnvExtension.Descr.tracksScopes {α β σ : Type} (descr : Descr α β σ) : Bool

Whether scope operations that change the effective state must be recorded like content changes; see State.scopeChanged.

def Lean.ScopedEnvExtension.Descr.noteScopeChange {α β σ : Type} (descr : Descr α β σ) (s : State σ) (b : β) : State σ

Notes on s that the entry b was added to it; see State.scopeChanged.

@[instance_reducible]

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} (descr : Descr α β σ) (env : Environment) (s : StateStack α β σ) : OLeanEntries (Array (Entry α))

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

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

@[instance_reducible]

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

Modifies delimitsLocal flag to false on the top depth entries of the state stack, to turn off delimiting of local entries across multiple implicit scope levels (e.g. those introduced by compound namespace A.B.C expansions).

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

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) (genRecorded : Bool := false) : σ

Returns the state in effect. For genRecorded, see EnvExtension.getState.

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.setDelimitsLocal {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (depth : Nat) : m Unit

Used to implement end_local_scope command, that disables delimiting local entries of ScopedEnvExtension across depth scope levels.

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 : σ → σ
• exportEntry? : Environment → α → OLeanEntries (Option α)
• trackGen : Bool

  See PersistentEnvExtensionDescrCore.trackGen.

• logWrites : Bool

  See EnvExtension.logWrites.

• entryDecl? : Option (α → Name)

  See ScopedEnvExtension.Descr.entryDecl?.

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