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

chore: add helper function

Browse source
This commit is contained in:
Leonardo de Moura 2023-07-11 07:37:52 -07:00 • committed by Leonardo de Moura
parent a3ebfe29ea
commit 264e376741
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/Hashable.lean
View file

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