From d6a7eb3987c612fed2df8a986883a079f7cefcfe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 17 Oct 2024 16:46:10 +0200 Subject: [PATCH] feat: add Hashable instance for Char (#5747) I needed this in downstream code, and it seems to make the most sense to just contribute it here. --- 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 28c382307c..da29eeffff 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -51,6 +51,9 @@ instance : Hashable USize where instance : Hashable (Fin n) where hash v := v.val.toUInt64 +instance : Hashable Char where + hash c := c.val.toUInt64 + instance : Hashable Int where hash | Int.ofNat n => UInt64.ofNat (2 * n)