Equations
- Lean.instHashablePtr = { hash := fun (a : Lean.Ptr α) => hash64 (ptrAddrUnsafe a).toUInt64 }
Equations
- Lean.instBEqPtr = { beq := fun (a b : Lean.Ptr α) => ptrAddrUnsafe a == ptrAddrUnsafe b }
Set of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
Equations
- Lean.PtrSet α = Lean.HashSet (Lean.Ptr α)
Instances For
Equations
- Lean.mkPtrSet capacity = Lean.mkHashSet capacity