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

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

Instances For

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

- state : σ
- activeScopes : NameSet
- delimitsLocal : Bool

Instances For

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

- map : SMap Name (PArray β)

Instances For

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

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

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

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

Instances For

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

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

Instances For

source
def Lean.ScopedEnvExtension.instInhabitedStateStack.default {a✝ a✝¹ a✝² : Type} :
StateStack a✝ a✝¹ a✝²
Equations

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

Instances For

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

- Lean.ScopedEnvExtension.instInhabitedStateStack = { default := Lean.ScopedEnvExtension.instInhabitedStateStack.default }

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

- name : Name
- mkInitial : IO σ
- ofOLeanEntry : σ → α → ImportM β
- toOLeanEntry : β → α
- addEntry : σ → β → σ
- finalizeImport : σ → σ
- exportEntry? : OLeanLevel → α → Option α

Instances For

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

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

source
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 }] }

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

- Lean.instInhabitedScopedEnvExtension = { default := Lean.instInhabitedScopedEnvExtension.default }

source
opaque Lean.scopedEnvExtensionsRef :
IO.Ref (Array (ScopedEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState))
source
unsafe def Lean.registerScopedEnvExtensionUnsafe {α β σ : Type} (descr : ScopedEnvExtension.Descr α β σ) :
IO (ScopedEnvExtension α β σ)
Equations

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

Instances For

source
@[implemented_by Lean.registerScopedEnvExtensionUnsafe]
opaque Lean.registerScopedEnvExtension {α β σ : Type} (descr : ScopedEnvExtension.Descr α β σ) :
IO (ScopedEnvExtension α β σ)
source
def Lean.ScopedEnvExtension.pushScope {α β σ : Type} (ext : ScopedEnvExtension α β σ) (env : Environment) :
Environment
Equations

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 = []

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Lean.SimpleScopedEnvExtension (α σ : Type) :
Type
Equations

- Lean.SimpleScopedEnvExtension α σ = Lean.ScopedEnvExtension α α σ

Instances For

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

- name : Name
- addEntry : σ → α → σ
- initial : σ
- finalizeImport : σ → σ
- exportEntry? : OLeanLevel → α → Option α

Instances For

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

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

Instances For