Documentation

Lean.ScopedEnvExtension

Instances For
Equations
  • Lean.ScopedEnvExtension.instInhabitedScopedEntries = { default := { map := default } }
structure Lean.ScopedEnvExtension.Descr (α β σ : Type) :
  • name : Lean.Name
  • mkInitial : IO σ
  • ofOLeanEntry : σαLean.ImportM β
  • toOLeanEntry : βα
  • addEntry : σβσ
  • finalizeImport : σσ
Instances For
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance Lean.instInhabitedScopedEnvExtension {a✝ : Type} [Inhabited a✝] {a✝¹ a✝² : Type} :
Inhabited (Lean.ScopedEnvExtension a✝ a✝¹ a✝²)
Equations
  • Lean.instInhabitedScopedEnvExtension = { default := { descr := default, ext := default } }
@[implemented_by Lean.registerScopedEnvExtensionUnsafe]
Equations
  • One or more equations did not get rendered due to their size.
def Lean.ScopedEnvExtension.addScopedEntry {α β σ : Type} (ext : Lean.ScopedEnvExtension α β σ) (env : Lean.Environment) (namespaceName : Lean.Name) (b : β) :
Equations
def Lean.ScopedEnvExtension.addCore {α β σ : Type} (env : Lean.Environment) (ext : Lean.ScopedEnvExtension α β σ) (b : β) (kind : Lean.AttributeKind) (namespaceName : Lean.Name) :
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Lean.activateScoped {m : TypeType} [Monad m] [Lean.MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (namespaceName : Lean.Name) :
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
  • name : Lean.Name
  • addEntry : σασ
  • initial : σ
  • finalizeImport : σσ
Equations
  • One or more equations did not get rendered due to their size.