From b521a65f5f1583c241b7bedc39ba5e4b3768a04c Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 14 Jan 2025 11:10:34 +0100 Subject: [PATCH] Added docstring that went missing during merge --- src/Std/Data/DHashMap/Internal/List/Associative.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index 6e6b5d22aba1..5d78184dcd09 100644 --- 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