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