structure Lean.Ptr (α : Type u) : Type u

• value : α

@[implicit_reducible]

unsafe instance Lean.instHashablePtr {α : Type u_1} : Hashable (Ptr α)

@[implicit_reducible]

unsafe instance Lean.instBEqPtr {α : Type u_1} : BEq (Ptr α)

unsafe def Lean.PtrSet (α : Type) : Type

Set of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.

unsafe def Lean.mkPtrSet {α : Type} (capacity : Nat := 64) : PtrSet α

@[reducible, inline]

unsafe abbrev Lean.PtrSet.insert {α : Type} (s : PtrSet α) (a : α) : PtrSet α

@[reducible, inline]

unsafe abbrev Lean.PtrSet.contains {α : Type} (s : PtrSet α) (a : α) : Bool

unsafe def Lean.PtrMap (α β : Type) : Type

Map of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.

unsafe def Lean.mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β

@[reducible, inline]

unsafe abbrev Lean.PtrMap.insert {α β : Type} (s : PtrMap α β) (a : α) (b : β) : PtrMap α β

@[reducible, inline]

unsafe abbrev Lean.PtrMap.contains {α β : Type} (s : PtrMap α β) (a : α) : Bool

@[reducible, inline]

unsafe abbrev Lean.PtrMap.find? {α β : Type} (s : PtrMap α β) (a : α) : Option β