From 43fa46412d2e9132ae44553cea0609736def0b4d Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 7 Aug 2024 15:36:19 +0200
Subject: [PATCH] feat: deprecated variants of hash map query methods (#4943)

#4917 will expose users of the `Lean` API to the renaming of the hash
map query methods. This PR aims to make the transition easier by adding
deprecated functions with the old names.
---
 src/Std/Data/HashMap/Basic.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index a975393edc..79577be2a8 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -112,6 +112,10 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map
 @[inline] def get? (m : HashMap α β) (a : α) : Option β :=
   DHashMap.Const.get? m.inner a
 
+@[deprecated get? "Use `m[a]?` or `m.get? a` instead", inherit_doc get?]
+def find? (m : HashMap α β) (a : α) : Option β :=
+  m.get? a
+
 @[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
     (a : α) : Bool :=
   m.inner.contains a
@@ -135,6 +139,10 @@ Retrieves the mapping for the given key. Ensures that such a mapping exists by r
     (fallback : β) : β :=
   DHashMap.Const.getD m.inner a fallback
 
+@[deprecated getD, inherit_doc getD]
+def findD (m : HashMap α β) (a : α) (fallback : β) : β :=
+  m.getD a fallback
+
 /--
 The notation `m[a]!` is preferred over calling this function directly.
 
@@ -143,6 +151,10 @@ Tries to retrieve the mapping for the given key, panicking if no such mapping is
 @[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
   DHashMap.Const.get! m.inner a
 
+@[deprecated get! "Use `m[a]!` or `m.get! a` instead", inherit_doc get!]
+def find! [Inhabited β] (m : HashMap α β) (a : α) : Option β :=
+  m.get! a
+
 instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) where
   getElem m a h := m.get a h
   getElem? m a := m.get? a