Further environment extension API; the primitives live in Lean.Environment
.
Simple PersistentEnvExtension
that implements exportEntriesFn
using a list of entries.
Equations
- Lean.SimplePersistentEnvExtension α σ = Lean.PersistentEnvExtension α α (List α × σ)
Instances For
Equations
- Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun (r : σ) (es : Array α) => Array.foldl (fun (r : σ) (e : α) => addEntryFn r e) r es) initState as
Instances For
- name : Name
- addEntryFn : σ → α → σ
- asyncMode : EnvExtension.AsyncMode
- exported : Bool
Whether entries should be imported into other modules. Entries are always accessible in the language server via
getModuleEntries (includeServer := true)
.
Instances For
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))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
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
Instances For
Get the current state of the given SimplePersistentEnvExtension
.
Equations
- ext.getState env asyncMode = (Lean.PersistentEnvExtension.getState ext env asyncMode).snd
Instances For
Set the current state of the given SimplePersistentEnvExtension
. This change is not persisted across files.
Equations
Instances For
Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.
Equations
Instances For
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
Instances For
Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 α))
- addEntryFn : NameMap α → Name × α → NameMap α
- exportEntriesFn : NameMap α → Array (Name × α)
- saveEntriesFn : NameMap α → Array (Name × α)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.