From c425397b45e9f2eeec1c4313ca3bc1861cc00c62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Oct 2021 17:19:39 -0700 Subject: [PATCH] feat: `Hashable` instances for `UInt8` and `UInt16` --- src/Init/Data/Hashable.lean | 6 ++++++ tests/lean/run/sarray.lean | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) 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)