Lean.ScopedEnvExtension

source

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

Type

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

source

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

Type

state : σ
activeScopes : Lean.NameSet

source

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

Type

map : Lean.SMap Lean.Name (Std.PArray β)

source

instance Lean.ScopedEnvExtension.instInhabitedScopedEntries:

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

Equations

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

source

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

Type

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

source

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

source

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

Type

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

source

instance Lean.ScopedEnvExtension.instInhabitedDescr {α : Type} {β : Type} {σ : Type} [inst : Inhabited α] :

Inhabited (Lean.ScopedEnvExtension.Descr α β σ)

Equations

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

source

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.

source

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

Lean.ScopedEnvExtension.ScopedEntries β

Equations

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

source

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.

source

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.

source

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)

source

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

Type

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

source

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

source

opaque Lean.scopedEnvExtensionsRef:

IO.Ref (Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))

source

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.

source

@[implementedBy Lean.registerScopedEnvExtensionUnsafe]

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

IO (Lean.ScopedEnvExtension α β σ)

source

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.

source

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.

source

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)

source

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

Lean.Environment

Equations

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

source

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.

source

def Lean.ScopedEnvExtension.add {m : Type → Type} {α : Type} {β : Type} {σ : Type} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : 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.

source

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

Equations

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

source

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

Lean.Environment

Equations

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

source

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.

source

def Lean.pushScope {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] :

m Unit

Equations

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

source

def Lean.popScope {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] :

m Unit

Equations

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

source

def Lean.activateScoped {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] (namespaceName : Lean.Name) :

m Unit

Equations

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

source

@[inline]

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

Type

Equations

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

source

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

Type

name : Lean.Name
addEntry : σ → α → σ
initial : σ
finalizeImport : σ → σ

source

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.