Skip to content

Commit 89c3079

Browse files
authoredAug 12, 2024
chore: fix typo in hash code for Expr equality test (leanprover#4990)
We observed a small performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean Before: 2.65s After: 2.60s
1 parent 37f9063 commit 89c3079

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed
 

‎src/kernel/expr_eq_fn.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ template<bool CompareBinderInfo>
2323
class expr_eq_fn {
2424
struct key_hasher {
2525
std::size_t operator()(std::pair<lean_object *, lean_object *> const & p) const {
26-
return hash((size_t)p.first >> 3, (size_t)p.first >> 3);
26+
return hash((size_t)p.first >> 3, (size_t)p.second >> 3);
2727
}
2828
};
2929
typedef std::unordered_set<std::pair<lean_object *, lean_object *>, key_hasher> cache;

0 commit comments

Comments
 (0)
Please sign in to comment.