From eca569f237f0b992781a4ccadd6df47be438a22f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Mar 2020 17:55:33 -0800
Subject: [PATCH] chore: use `NonScalar`

---
 src/Init/ShareCommon.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/Init/ShareCommon.lean b/src/Init/ShareCommon.lean
index bcb6cc5e8b..7514c93f9b 100644
--- a/src/Init/ShareCommon.lean
+++ b/src/Init/ShareCommon.lean
@@ -21,10 +21,7 @@ namespace ShareCommon
   `PersistentHashMap` and `PersistentHashSet`.
   These maps and sets are "instantiated here using the "unsafe"
   primitives `Object.eq`, `Object.hash`, and `ptrAddrUnsafe`. -/
-
-constant ObjectPointed : PointedType := arbitrary _
-def Object : Type := ObjectPointed.type
-instance Object.inhabited : Inhabited Object := ⟨ObjectPointed.val⟩
+abbrev Object : Type := NonScalar
 
 unsafe def Object.ptrEq (a b : Object) : Bool :=
 ptrAddrUnsafe a == ptrAddrUnsafe b