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

Equations

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

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

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

Equations

• descr.tracksScopes = (descr.trackGen || descr.logWrites)

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.

Equations

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

@[instance_reducible]

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 α β σ) (env : Environment) (s : StateStack α β σ) : OLeanEntries (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_reducible]

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

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) ext.ext.toEnvExtension.asyncMode Lean.Name.anonymous (Lean.ScopedEnvExtension.writeLog✝ ext b)

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

Equations

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

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

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

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] (depth : Nat) : m Unit

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

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? : 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 α σ)

Equations

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