From 6d63f6305eee006f1acaddff2f36654c98ce5b5e Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 4 Feb 2025 15:40:31 +0100
Subject: [PATCH] feat: add `Hashable` instances for `PUnit` and `PEmpty`
 (#6866)

This PR adds missing `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 e964c7c342..093c9256be 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