From d0a2e138d0eb28b004dea69330024afd80b6c5ce Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Thu, 30 Jan 2025 11:01:29 +0100
Subject: [PATCH] add Hashable instances for PUnit and PEmpty
---
src/Init/Data/Hashable.lean | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index e964c7c342cc..093c9256bef4 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -22,6 +22,12 @@ instance : Hashable Bool where
| true => 11
| false => 13
+instance : Hashable PEmpty.{u} where
+ hash x := nomatch x
+
+instance : Hashable PUnit.{u} where
+ hash | .unit => 11
+
instance [Hashable α] : Hashable (Option α) where
hash
| none => 11