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.