max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2021-06-02 08:06:52 -07:00
parent d841c2e1d8
commit d435b435c5
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/Name.lean
View file

@ -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

4
src/util/name.cpp
View file

@ -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) {

2
src/util/name.h
View file

@ -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);