add Hashable instances for PUnit and PEmpty

leanprover · Jan 30, 2025 · d0a2e13 · d0a2e13
1 parent dc445d7
commit d0a2e13
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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