Documentation

Lean.Util.PtrSet

structure Lean.Ptr (α : Type u) :
  • value : α
Instances For
unsafe instance Lean.instHashablePtr {α : Type u_1} :
unsafe instance Lean.instBEqPtr {α : Type u_1} :
unsafe def Lean.PtrSet (α : Type) :

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

unsafe def Lean.mkPtrSet {α : Type} (capacity : Nat := 64) :
@[reducible, inline]
unsafe abbrev Lean.PtrSet.insert {α : Type} (s : Lean.PtrSet α) (a : α) :
@[reducible, inline]
unsafe abbrev Lean.PtrSet.contains {α : Type} (s : Lean.PtrSet α) (a : α) :
unsafe def Lean.PtrMap (α β : Type) :

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

unsafe def Lean.mkPtrMap {α β : Type} (capacity : Nat := 64) :
@[reducible, inline]
unsafe abbrev Lean.PtrMap.insert {α β : Type} (s : Lean.PtrMap α β) (a : α) (b : β) :
@[reducible, inline]
unsafe abbrev Lean.PtrMap.contains {α β : Type} (s : Lean.PtrMap α β) (a : α) :
@[reducible, inline]
unsafe abbrev Lean.PtrMap.find? {α β : Type} (s : Lean.PtrMap α β) (a : α) :