From 684554e979ddaadda23b81ce03302f85fa1cf013 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Feb 2020 11:00:50 -0800
Subject: [PATCH] feat: add `PtrEqResult`

---
 src/Init/Core.lean | 12 ------------
 src/Init/Util.lean | 12 ++++++++----
 2 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index f6819102ba..934bcb87c3 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -306,18 +306,6 @@ abbrev DecidableEq (α : Sort u) :=
 def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
 s a b
 
-class inductive SemiDeciable (p : Prop)
-| unknown {}     : SemiDeciable
-| isTrue (h : p) : SemiDeciable
-
-def Decidable.toSemiDecidable {p : Prop} (d : Decidable p) : SemiDeciable p :=
-match d with
-| Decidable.isTrue h => SemiDeciable.isTrue h
-| _                  => SemiDeciable.unknown
-
-instance SemiDeciable.ofDecidable {p : Prop} [d : Decidable p] : SemiDeciable p :=
-d.toSemiDecidable
-
 inductive Option (α : Type u)
 | none {} : Option
 | some (val : α) : Option
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index da27eb675e..fb6dc88ee2 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -47,8 +47,12 @@ k (ptrAddrUnsafe a)
 @[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
 if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
 
-@[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : SemiDeciable (a = b) → β) : β :=
-if ptrAddrUnsafe a == ptrAddrUnsafe b then k (SemiDeciable.isTrue lcProof) else k SemiDeciable.unknown
+inductive PtrEqResult {α : Type u} (x y : α) : Prop
+| unknown {}          : PtrEqResult
+| yes     (h : x = y) : PtrEqResult
+
+@[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
+if ptrAddrUnsafe a == ptrAddrUnsafe b then k (PtrEqResult.yes lcProof) else k PtrEqResult.unknown
 
 @[implementedBy withPtrEqUnsafe]
 def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
@@ -63,8 +67,8 @@ condEq b
 
 /-- Similar to `withPtrEq`, but executes the continuation `k` with the "result" of the pointer equality test. -/
 @[implementedBy withPtrEqResultUnsafe]
-def withPtrEqResult {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : SemiDeciable (a = b) → β) : β :=
-k SemiDeciable.unknown
+def withPtrEqResult {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
+k PtrEqResult.unknown
 
 @[implementedBy withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=