diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index 931725006d..3f81ec033e 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -27,6 +27,12 @@ instance [Hashable α] : Hashable (Option α) where instance [Hashable α] : Hashable (List α) where hash as := as.foldl (fun r a => mixHash r (hash a)) 7 +instance : Hashable UInt8 where + hash n := n.toUInt64 + +instance : Hashable UInt16 where + hash n := n.toUInt64 + instance : Hashable UInt32 where hash n := n.toUInt64 diff --git a/tests/lean/run/sarray.lean b/tests/lean/run/sarray.lean index 191eeb9d6d..ebfafc00ee 100644 --- a/tests/lean/run/sarray.lean +++ b/tests/lean/run/sarray.lean @@ -34,4 +34,4 @@ def tst3 (n : Nat) (expected : UInt32) : IO Unit := do set_option trace.compiler.ir.result true in def computeByteHash (bytes : ByteArray) := - bytes.foldl (init := 1723) fun h b => mixHash h (hash b.toNat) + bytes.foldl (init := 1723) fun h b => mixHash h (hash b)