From e28bfedae200fd3a9c6ee4604199d612a5ffb5e7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 27 Sep 2024 15:59:36 +0200 Subject: [PATCH] doc: remove inaccurate `PersistentEnvExtension.setState/modifyState` claim Likely a copy-paste mistake Fixes #3039 --- src/Lean/Environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 9a7a723fee..0b0c88f565 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -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) }