From d435b435c51f3c49df08f8bee68ff3b3dffc07a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Jun 2021 08:06:52 -0700
Subject: [PATCH] chore: remove workaround

---
 src/Lean/Data/Name.lean | 4 ++--
 src/util/name.cpp       | 4 ++--
 src/util/name.h         | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 17d43a8bbd..c853d9b55c 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -12,8 +12,8 @@ instance : Coe String Name := ⟨Name.mkSimple⟩
 
 namespace Name
 
-@[export lean_name_hash] def hashEx : Name → USize :=
-  fun n => Name.hash n |>.toUSize
+@[export lean_name_hash] def hashEx : Name → UInt64 :=
+  Name.hash
 
 def getPrefix : Name → Name
   | anonymous => anonymous
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 08cfcbab76..d066423404 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -27,8 +27,8 @@ static inline obj_res name_mk_string_of_cstr(obj_arg p, char const * s) {
     return lean_name_mk_string(p, mk_string(s));
 }
 
-extern "C" usize lean_name_hash(obj_arg n);
-usize name::hash(b_obj_arg n) { inc(n); return lean_name_hash(n); }
+extern "C" uint64_t lean_name_hash(obj_arg n);
+uint64_t name::hash(b_obj_arg n) { inc(n); return lean_name_hash(n); }
 
 bool name::eq_core(b_obj_arg n1, b_obj_arg n2) {
     while (true) {
diff --git a/src/util/name.h b/src/util/name.h
index b32f601723..143bf5336b 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -99,7 +99,7 @@ public:
     static name mk_internal_unique_name();
     name & operator=(name const & other) { object_ref::operator=(other); return *this; }
     name & operator=(name && other) { object_ref::operator=(other); return *this; }
-    static usize hash(b_obj_arg n);
+    static uint64_t hash(b_obj_arg n);
     unsigned hash() const { return hash(raw()); }
     /** \brief Return true iff \c n1 is a prefix of \c n2. */
     friend bool is_prefix_of(name const & n1, name const & n2);