Extra utilities for environment extensions #
def
Lean.SimplePersistentEnvExtension.modifyEntries
{α σ : Type}
(env : Environment)
(ext : SimplePersistentEnvExtension α σ)
(f : List α → List α)
(asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode)
(asyncDecl : Name := Name.anonymous)
:
Modifies the List α of entries of a SimplePersistentEnvExtension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.SimplePersistentEnvExtension.setEntries
{α σ : Type}
(env : Environment)
(ext : SimplePersistentEnvExtension α σ)
(entries : List α)
(asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode)
(asyncDecl : Name := Name.anonymous)
:
Sets the List α of entries of a SimplePersistentEnvExtension.
Equations
- One or more equations did not get rendered due to their size.