Documentation

Lean.Util.PtrSet

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

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

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

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

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