From a2a39882d540bc92de46d345372886637697cc5f Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Wed, 31 Aug 2022 13:38:55 +0200 Subject: [PATCH] feat: add Hashable for Subtype --- src/Init/Prelude.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b9343f4bdd..9ae195c2ee 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3244,6 +3244,9 @@ def USize.toUInt64 (u : USize) : UInt64 where @[extern "lean_uint64_mix_hash"] opaque mixHash (u₁ u₂ : UInt64) : UInt64 +instance [Hashable α] {p : α → Prop} : Hashable (Subtype p) where + hash a := hash a.val + /-- A opaque string hash function. -/ @[extern "lean_string_hash"] protected opaque String.hash (s : @& String) : UInt64