From 0f8b59eed710e032fc7bccdca3225203449086ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Feb 2020 11:22:17 -0800
Subject: [PATCH] fix: typo `Prop` => `Type`

---
 src/Init/Util.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index fb6dc88ee2..f564f9ac1c 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -47,7 +47,7 @@ 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 ()
 
-inductive PtrEqResult {α : Type u} (x y : α) : Prop
+inductive PtrEqResult {α : Type u} (x y : α) : Type
 | unknown {}          : PtrEqResult
 | yes     (h : x = y) : PtrEqResult