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