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

• value : α

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

Equations

• Lean.instHashablePtr = { hash := fun (a : Lean.Ptr α) => hash64 (ptrAddrUnsafe a).toUInt64 }

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

Equations

• Lean.instBEqPtr = { beq := fun (a b : Lean.Ptr α) => ptrAddrUnsafe a == ptrAddrUnsafe b }

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

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

Equations

• Lean.PtrSet α = Lean.HashSet (Lean.Ptr α)

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

Equations

• Lean.mkPtrSet capacity = Lean.mkHashSet capacity

@[reducible, inline]

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

Equations

• s.insert a = Lean.HashSet.insert s { value := a }

@[reducible, inline]

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

Equations

• s.contains a = Lean.HashSet.contains s { value := a }

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

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

Equations

• Lean.PtrMap α β = Lean.HashMap (Lean.Ptr α) β

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

Equations

• Lean.mkPtrMap capacity = Lean.mkHashMap capacity

@[reducible, inline]

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

Equations

• s.insert a b = Lean.HashMap.insert s { value := a } b

@[reducible, inline]

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

Equations

• s.contains a = Lean.HashMap.contains s { value := a }

@[reducible, inline]

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

Equations

• s.find? a = Lean.HashMap.find? s { value := a }