From 73cb952275ea0ddc58701db1e50cb0bfbaf42d16 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 May 2022 15:01:32 -0700 Subject: [PATCH] =?UTF-8?q?feat:=20add=20`Hashable=20(Array=20=CE=B1)`=20i?= =?UTF-8?q?nstance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Init/Data/Hashable.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index e871dcb40a..f661c8737a 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -30,6 +30,9 @@ instance [Hashable α] : Hashable (Option α) where instance [Hashable α] : Hashable (List α) where hash as := as.foldl (fun r a => mixHash r (hash a)) 7 +instance [Hashable α] : Hashable (Array α) where + hash as := as.foldl (fun r a => mixHash r (hash a)) 7 + instance : Hashable UInt8 where hash n := n.toUInt64