From 264e37674116fa5de43fd671db7af2ccffbba87c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 11 Jul 2023 07:37:52 -0700
Subject: [PATCH] chore: add helper function

---
 src/Init/Data/Hashable.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index d32ed5cc67..0b4e65bf06 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -58,3 +58,7 @@ instance : Hashable Int where
 
 instance (P : Prop) : Hashable P where
   hash _ := 0
+
+/-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
+@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
+  mixHash u 11