From 9efe4e2d1989d685d53ccb575e3dd472a2fd4cab Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 09:54:39 +1000 Subject: [PATCH] chore(HashMap): deprecate unused API additions --- Mathlib/Data/HashMap.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Data/HashMap.lean b/Mathlib/Data/HashMap.lean index 7929e522e2f81..8dc272f5d2e1d 100644 --- a/Mathlib/Data/HashMap.lean +++ b/Mathlib/Data/HashMap.lean @@ -29,14 +29,17 @@ namespace Batteries.HashMap variable [BEq α] [Hashable α] /-- The list of keys in a `HashMap`. -/ +@[deprecated "Cleaning up unused API additions in Mathlib." (since := "2024-06-12")] def keys (m : HashMap α β) : List α := m.fold (fun ks k _ => k :: ks) [] /-- The list of values in a `HashMap`. -/ +@[deprecated "Cleaning up unused API additions in Mathlib." (since := "2024-06-12")] def values (m : HashMap α β) : List β := m.fold (fun vs _ v => v :: vs) [] /-- Add a value to a `HashMap α (List β)` viewed as a multimap. -/ +@[deprecated "Cleaning up unused API additions in Mathlib." (since := "2024-06-12")] def consVal (self : HashMap α (List β)) (a : α) (b : β) : HashMap α (List β) := match self.find? a with | none => self.insert a [b]