Skip to content

Commit

Permalink
doc: remove inaccurate PersistentEnvExtension.setState/modifyState
Browse files Browse the repository at this point in the history
…claim

Likely a copy-paste mistake

Fixes #3039
  • Loading branch information
Kha authored Sep 27, 2024
1 parent e7691f3 commit e28bfed
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Lean/Environment.lean
Original file line number Diff line number Diff line change
Expand Up @@ -515,11 +515,11 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
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. -/
/-- Set the current state of the given extension in the given environment. -/
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. -/
/-- Modify the state of the given extension in the given environment by applying the given function. -/
def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) : Environment :=
ext.toEnvExtension.modifyState env fun ps => { ps with state := f (ps.state) }

Expand Down

0 comments on commit e28bfed

Please sign in to comment.