Added docstring that went missing during merge

leanprover · Jan 14, 2025 · b521a65 · b521a65
1 parent 317b351
commit b521a65
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -2695,6 +2695,7 @@ theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
 
 end
 
+/-- Internal implementation detail of the hash map -/
 def alterKey [BEq α] [LawfulBEq α] (k : α) (f : Option (β k) → Option (β k))
     (l : List ((a : α) × β a)) : List ((a : α) × β a) :=
   match f (getValueCast? k l) with