max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add docstrings in PersistentExtension

Browse source 
Add docstring to functions with non-obvious persistence properties. See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/HashMap.20extension/near/300784691
This commit is contained in:
Patrick Massot 2022-09-26 21:23:44 +02:00 • committed by Leonardo de Moura
parent f067382f52
commit f0c8e6fa2d
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Environment.lean
View file

@ -423,12 +423,15 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
let state := ext.addEntryFn s.state b;
{ s with state := state }
/-- Get the current state of the given extension in the given environment. -/
def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : σ :=
(ext.toEnvExtension.getState env).state
/-- Set the current state of the given extension in the given environment. This change is *not* persisted across files. -/
def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=
ext.toEnvExtension.modifyState env fun ps => { ps with state := s }
/-- Modify the state of the given extension in the given environment by applying the given function. This change is *not* persisted across files. -/
def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) : Environment :=
ext.toEnvExtension.modifyState env fun ps => { ps with state := f (ps.state) }
@ -505,9 +508,11 @@ def getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension
def getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) : σ :=
(PersistentEnvExtension.getState ext env).2
/-- Set the current state of the given `SimplePersistentEnvExtension`. This change is *not* persisted across files. -/
def setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) : Environment :=
PersistentEnvExtension.modifyState ext env (fun ⟨entries, _⟩ => (entries, s))
/-- Modify the state of the given extension in the given environment by applying the given function. This change is *not* persisted across files. -/
def modifyState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) : Environment :=
PersistentEnvExtension.modifyState ext env (fun ⟨entries, s⟩ => (entries, f s))