From 3ebb4e76eec972eeea0b2a45e5997c318d0e5d4d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Feb 2020 15:53:30 -0800
Subject: [PATCH] feat: more general `withPtrEq`

---
 src/Init/Util.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index c92d7d90b6..f00c12ff03 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -41,15 +41,15 @@ panic! "unreachable"
 @[extern "lean_ptr_addr"]
 unsafe def ptrAddrUnsafe {α : Type u} (a : @& α) : USize := 0
 
-@[inline] unsafe def withPtrEqUnsafe {α : Type u} (r : α → α → Bool) (h : ∀ a, r a a = true) : α → α → Bool :=
-fun a b => if ptrAddrUnsafe a == ptrAddrUnsafe b then true else r a b
-
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
 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 ()
+
 @[implementedBy withPtrEqUnsafe]
-def withPtrEq {α : Type u} (r : α → α → Bool) (h : ∀ a, r a a = true) : α → α → Bool :=
-r
+def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
+k ()
 
 @[implementedBy withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=