Documentation

Lean.ScopedEnvExtension

inductive Lean.ScopedEnvExtension.Entry (α : Type) :
Type
structure Lean.ScopedEnvExtension.State (σ : Type) :
Type
Equations
  • Lean.ScopedEnvExtension.instInhabitedScopedEntries = { default := { map := default } }
structure Lean.ScopedEnvExtension.StateStack (α : Type) (β : Type) (σ : Type) :
Type
Equations
  • Lean.ScopedEnvExtension.instInhabitedStateStack = { default := { stateStack := default, scopedEntries := default, newEntries := default } }
structure Lean.ScopedEnvExtension.Descr (α : Type) (β : Type) (σ : Type) :
Type
  • name : Lean.Name
  • mkInitial : IO σ
  • ofOLeanEntry : σαLean.ImportM β
  • toOLeanEntry : βα
  • addEntry : σβσ
  • finalizeImport : σσ
instance Lean.ScopedEnvExtension.instInhabitedDescr {α : Type} {β : Type} {σ : Type} [inst : Inhabited α] :
Equations
  • Lean.ScopedEnvExtension.instInhabitedDescr = { default := { name := default, mkInitial := default, ofOLeanEntry := default, toOLeanEntry := default, addEntry := fun s x => s, finalizeImport := id } }
def Lean.ScopedEnvExtension.mkInitial {α : Type} {β : Type} {σ : Type} (descr : Lean.ScopedEnvExtension.Descr α β σ) :
Equations
Equations
Equations
Equations
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 } }
unsafe def Lean.registerScopedEnvExtensionUnsafe {α : Type} {β : Type} {σ : Type} (descr : Lean.ScopedEnvExtension.Descr α β σ) :
Equations
@[implementedBy Lean.registerScopedEnvExtensionUnsafe]
constant Lean.registerScopedEnvExtension {α : Type} {β : Type} {σ : Type} (descr : Lean.ScopedEnvExtension.Descr α β σ) :
def Lean.ScopedEnvExtension.pushScope {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) :
Equations
def Lean.ScopedEnvExtension.popScope {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) :
Equations
def Lean.ScopedEnvExtension.addScopedEntry {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) (namespaceName : Lean.Name) (b : β) :
Equations
def Lean.ScopedEnvExtension.addLocalEntry {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) (b : β) :
Equations
def Lean.ScopedEnvExtension.getState {σ : Type} {α : Type} {β : Type} [inst : Inhabited σ] (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) :
σ
Equations
def Lean.ScopedEnvExtension.activateScoped {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) (namespaceName : Lean.Name) :
Equations
def Lean.ScopedEnvExtension.modifyState {α : Type} {β : Type} {σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) (f : σσ) :
Equations
def Lean.pushScope {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] :
Equations
def Lean.popScope {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] :
Equations
def Lean.activateScoped {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadLiftT (ST IO.RealWorld) m] (namespaceName : Lean.Name) :
Equations
@[inline]
abbrev Lean.SimpleScopedEnvExtension (α : Type) (σ : Type) :
Type
Equations
structure Lean.SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) :
Type
  • name : Lean.Name
  • addEntry : σασ
  • initial : σ
  • finalizeImport : σσ
Equations