feat: basic instances for ULift and PLift (leanprover#5112)

opencompl · Aug 21, 2024 · 0a8d1bf · 0a8d1bf
1 parent a58da12
commit 0a8d1bf
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 0 deletions.
diff --git a/src/Init/Data.lean b/src/Init/Data.lean
@@ -37,3 +37,5 @@ import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift
diff --git a/src/Init/Data/PLift.lean b/src/Init/Data/PLift.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for PLift
+
+instance [Subsingleton α] : Subsingleton (PLift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg PLift.up (Subsingleton.elim a b)
diff --git a/src/Init/Data/ULift.lean b/src/Init/Data/ULift.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for ULift
+
+instance [Subsingleton α] : Subsingleton (ULift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg ULift.up (Subsingleton.elim a b)