From b379bca28bb509eb4f787995a8939f709e53cf03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Mar 2020 08:29:31 -0800
Subject: [PATCH] chore: rename `PtrEqResult.yes` ==> `PtrEqResult.yesEqual`

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

diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index f564f9ac1c..b71ac3f860 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -48,11 +48,11 @@ k (ptrAddrUnsafe a)
 if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
 
 inductive PtrEqResult {α : Type u} (x y : α) : Type
-| unknown {}          : PtrEqResult
-| yes     (h : x = y) : PtrEqResult
+| unknown {}           : PtrEqResult
+| yesEqual (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
+if ptrAddrUnsafe a == ptrAddrUnsafe b then k (PtrEqResult.yesEqual lcProof) else k PtrEqResult.unknown
 
 @[implementedBy withPtrEqUnsafe]
 def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=