- global: {α : Type} → α → Lean.ScopedEnvExtension.Entry α
- scoped: {α : Type} → Lake.Name → α → Lean.ScopedEnvExtension.Entry α
Instances For
- state : σ
- activeScopes : Lean.NameSet
Instances For
- map : Lean.SMap Lake.Name (Lean.PArray β)
Instances For
- stateStack : List (Lean.ScopedEnvExtension.State σ)
- scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β
- newEntries : List (Lean.ScopedEnvExtension.Entry α)
Instances For
instance
Lean.ScopedEnvExtension.instInhabitedStateStack :
{a a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension.StateStack a a_1 a_2)
- name : Lake.Name
- mkInitial : IO σ
- ofOLeanEntry : σ → α → Lean.ImportM β
- toOLeanEntry : β → α
- addEntry : σ → β → σ
- finalizeImport : σ → σ
Instances For
instance
Lean.ScopedEnvExtension.instInhabitedDescr
{α : Type}
{β : Type}
{σ : Type}
[Inhabited α]
:
def
Lean.ScopedEnvExtension.mkInitial
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension.StateStack α β σ)
Instances For
def
Lean.ScopedEnvExtension.ScopedEntries.insert
{β : Type}
(scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β)
(ns : Lake.Name)
(b : β)
:
Instances For
def
Lean.ScopedEnvExtension.addImportedFn
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
(as : Array (Array (Lean.ScopedEnvExtension.Entry α)))
:
Instances For
def
Lean.ScopedEnvExtension.addEntryFn
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
(s : Lean.ScopedEnvExtension.StateStack α β σ)
(e : Lean.ScopedEnvExtension.Entry β)
:
Instances For
def
Lean.ScopedEnvExtension.exportEntriesFn
{α : Type}
{β : Type}
{σ : Type}
(s : Lean.ScopedEnvExtension.StateStack α β σ)
:
Instances For
- descr : Lean.ScopedEnvExtension.Descr α β σ
Instances For
instance
Lean.instInhabitedScopedEnvExtension :
{a : Type} → [inst : Inhabited a] → {a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension a a_1 a_2)
unsafe def
Lean.registerScopedEnvExtensionUnsafe
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension α β σ)
Instances For
@[implemented_by Lean.registerScopedEnvExtensionUnsafe]
opaque
Lean.registerScopedEnvExtension
{α : Type}
{β : Type}
{σ : Type}
(descr : Lean.ScopedEnvExtension.Descr α β σ)
:
IO (Lean.ScopedEnvExtension α β σ)
def
Lean.ScopedEnvExtension.pushScope
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
Instances For
def
Lean.ScopedEnvExtension.popScope
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
Instances For
def
Lean.ScopedEnvExtension.addEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(b : β)
:
Instances For
def
Lean.ScopedEnvExtension.addScopedEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(namespaceName : Lake.Name)
(b : β)
:
Instances For
def
Lean.ScopedEnvExtension.addLocalEntry
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(b : β)
:
Instances For
def
Lean.ScopedEnvExtension.add
{m : Type → Type}
{α : Type}
{β : Type}
{σ : Type}
[Monad m]
[Lean.MonadResolveName m]
[Lean.MonadEnv m]
(ext : Lean.ScopedEnvExtension α β σ)
(b : β)
(kind : optParam Lean.AttributeKind Lean.AttributeKind.global)
:
m Unit
Instances For
def
Lean.ScopedEnvExtension.getState
{σ : Type}
{α : Type}
{β : Type}
[Inhabited σ]
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
:
σ
Instances For
def
Lean.ScopedEnvExtension.activateScoped
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(namespaceName : Lake.Name)
:
Instances For
def
Lean.ScopedEnvExtension.modifyState
{α : Type}
{β : Type}
{σ : Type}
(ext : Lean.ScopedEnvExtension α β σ)
(env : Lean.Environment)
(f : σ → σ)
:
Instances For
def
Lean.pushScope
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[MonadLiftT (ST IO.RealWorld) m]
:
m Unit
Instances For
def
Lean.popScope
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[MonadLiftT (ST IO.RealWorld) m]
:
m Unit
Instances For
def
Lean.activateScoped
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[MonadLiftT (ST IO.RealWorld) m]
(namespaceName : Lake.Name)
:
m Unit
Instances For
@[inline, reducible]
Instances For
def
Lean.registerSimpleScopedEnvExtension
{α : Type}
{σ : Type}
(descr : Lean.SimpleScopedEnvExtension.Descr α σ)
: