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.

Equations

• Lean.SimplePersistentEnvExtension α σ = Lean.PersistentEnvExtension α α (List α × σ)

@[specialize #[]]

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

Equations

• Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun (r : σ) (es : Array α) => Array.foldl (fun (r : σ) (e : α) => addEntryFn r e) r es) initState as

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

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

  See EnvExtension.logWrites.

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.

Equations

• Lean.SimplePersistentEnvExtension.replayOfFilter p addEntryFn newEntries x✝ s = (List.filter (p s) newEntries, List.foldl addEntryFn s (List.filter (p s) newEntries))

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• Lean.SimplePersistentEnvExtension.instInhabited = { default := Lean.SimplePersistentEnvExtension.instInhabited._aux_1 }

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

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

Equations

• ext.getEntries env asyncMode = (Lean.PersistentEnvExtension.getState ext env asyncMode).fst

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

Get the current state of the given SimplePersistentEnvExtension.

Equations

• ext.getState env asyncMode asyncDecl = (Lean.PersistentEnvExtension.getState ext env asyncMode asyncDecl).snd

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.

Equations

• ext.setState env s = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, snd) => (entries, s)

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.

Equations

• ext.modifyState env f = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, s) => (entries, f s)

def Lean.TagDeclarationExtension : Type

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

Equations

• Lean.TagDeclarationExtension = Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.TagDeclarationExtension.instInhabited : Inhabited TagDeclarationExtension

Equations

• Lean.TagDeclarationExtension.instInhabited = { default := Lean.TagDeclarationExtension.instInhabited._aux_1 }

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.TagDeclarationExtension.isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) : Bool

Equations

• One or more equations did not get rendered due to their size.

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 : Environment → NameMap α → OLeanEntries (Array (Name × α))
• statsFn : NameMap α → Format

@[instance_reducible]

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

Equations

• Lean.instInhabitedMapDeclarationExtension = { default := Lean.instInhabitedMapDeclarationExtension.default }

def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.async AsyncBranch.mainEnv) (logWrites : Bool := false) (exportEntriesFn : Environment → NameMap α → OLeanEntries (Array (Name × α)) := fun (env : Environment) (s : NameMap α) => have all := Array.filter (fun (x : Name × α) => match x with | (n, snd) => env.contains n false) (Std.TreeMap.toArray s); have exported := Array.filter (fun (x : Name × α) => match x with | (n, snd) => (env.setExporting true).contains n false) all; { exported := exported, server := exported, «private» := all }) : IO (MapDeclarationExtension α)

Equations

• One or more equations did not get rendered due to their size.

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

Adds the entry for declName. Entries are write-once: facts derived from an entry, such as cached type class resolution results, assume it never changes. allowOverwrite permits replacing an existing entry, which invalidates such facts; use it only where that is justified, and say why.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MapDeclarationExtension.find? {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) (level : OLeanLevel := OLeanLevel.exported) : Option α

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.