max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use NonScalar

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-02 17:55:33 -08:00
parent f607e9c478
commit eca569f237
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/ShareCommon.lean
View file

@ -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