Further environment extension API; the primitives live in Lean.Environment.

def Lean.SimplePersistentEnvExtension (α σ : Type) : Type

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

@[specialize #[]]

def Lean.mkStateFromImportedEntries {α σ : Type} (addEntryFn : σ → α → σ) (initState : σ) (as : Array (Array α)) : σ

structure Lean.SimplePersistentEnvExtensionDescr (α σ : Type) : Type

• name : Name
• addEntryFn : σ → α → σ
• addImportedFn : Array (Array α) → σ
• toArrayFn : List α → Array α
• asyncMode : EnvExtension.AsyncMode
• replay? : Option (List α → σ → σ → List α × σ)
• exported : Bool

  Whether entries should be imported into other modules. Entries are always accessible in the language server via getModuleEntries (includeServer := true).

def Lean.SimplePersistentEnvExtension.replayOfFilter {σ : Type u_1} {α : Type u_2} (p : σ → α → Bool) (addEntryFn : σ → α → σ) : List α → σ → σ → List α × σ

Returns a function suitable for SimplePersistentEnvExtensionDescr.replay? that replays all new entries onto the state using addEntryFn. p should filter out entries that have already been added to the state by a prior replay of the same realizable constant.

def Lean.registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : SimplePersistentEnvExtensionDescr α σ) : IO (SimplePersistentEnvExtension α σ)

instance Lean.SimplePersistentEnvExtension.instInhabited {α σ : Type} [Inhabited σ] : Inhabited (SimplePersistentEnvExtension α σ)

def Lean.SimplePersistentEnvExtension.getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) : List α

Get the list of values used to update the state of the given SimplePersistentEnvExtension in the current file.

def Lean.SimplePersistentEnvExtension.getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) : σ

Get the current state of the given SimplePersistentEnvExtension.

def Lean.SimplePersistentEnvExtension.setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) : Environment

Set the current state of the given SimplePersistentEnvExtension. This change is not persisted across files.

def Lean.SimplePersistentEnvExtension.modifyState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) : Environment

Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.

def Lean.SimplePersistentEnvExtension.findStateAsync {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) (declPrefix : Name) : σ

Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

def Lean.TagDeclarationExtension : Type

Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.

def Lean.mkTagDeclarationExtension (name : Name := by exact decl_name%) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.mainOnly) : IO TagDeclarationExtension

instance Lean.TagDeclarationExtension.instInhabited : Inhabited TagDeclarationExtension

def Lean.TagDeclarationExtension.tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Environment

def Lean.TagDeclarationExtension.isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Bool

structure Lean.MapDeclarationExtension (α : Type) extends Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α) : Type

Environment extension for mapping declarations to values. Declarations must only be inserted into the mapping in the module where they were declared.

• toEnvExtension : EnvExtension (PersistentEnvExtensionState (Name × α) (NameMap α))
• name : Name
• addImportedFn : Array (Array (Name × α)) → ImportM (NameMap α)
• addEntryFn : NameMap α → Name × α → NameMap α
• exportEntriesFn : NameMap α → Array (Name × α)
• saveEntriesFn : NameMap α → Array (Name × α)
• statsFn : NameMap α → Format

instance Lean.instInhabitedMapDeclarationExtension {a✝ : Type} : Inhabited (MapDeclarationExtension a✝)

def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) (exportEntriesFn : NameMap α → Array (Name × α) := fun (x : NameMap α) => RBMap.toArray x) : IO (MapDeclarationExtension α)

def Lean.MapDeclarationExtension.insert {α : Type} (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment

def Lean.MapDeclarationExtension.find? {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (includeServer : Bool := false) : Option α

def Lean.MapDeclarationExtension.contains {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Bool