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 α × σ)

Instances For

• Lean.SimplePersistentEnvExtension.instInhabited

@[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 α
• 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.

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 Lean.SimplePersistentEnvExtension.instInhabited {α σ : Type} [Inhabited σ] : Inhabited (SimplePersistentEnvExtension α σ)

Equations

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

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.

Equations

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

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

Get the current state of the given SimplePersistentEnvExtension.

Equations

• ext.getState env asyncMode = (Lean.PersistentEnvExtension.getState ext env asyncMode).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.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.

Equations

• ext.findStateAsync env declPrefix = (Lean.PersistentEnvExtension.findStateAsync ext env declPrefix).snd

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

Instances For

• Lean.TagDeclarationExtension.instInhabited

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

Equations

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

instance Lean.TagDeclarationExtension.instInhabited : Inhabited TagDeclarationExtension

Equations

• Lean.TagDeclarationExtension.instInhabited = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet))

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

Instances For

• Lean.instInhabitedMapDeclarationExtension

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

Equations

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

def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) (exportEntriesFn : NameMap α → Array (Name × α) := fun (x : NameMap α) => RBMap.toArray x) : 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 : α) : Environment

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) (includeServer : Bool := false) : 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) : Bool

Equations

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