From f0c8e6fa2d2f3580ac30bd217f20bf8572628565 Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Mon, 26 Sep 2022 21:23:44 +0200
Subject: [PATCH] doc: add docstrings in PersistentExtension

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
---
 src/Lean/Environment.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 1292d4a352..7767c4b740 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -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))