Documentation

Lean.Data.PersistentHashSet

structure Lean.PersistentHashSet (α : Type u) [BEq α] [Hashable α] :
Instances For
    @[reducible, inline]
    abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] :
    Equations
    Instances For
      @[inline]
      Equations
      • Lean.PersistentHashSet.empty = { set := Lean.PersistentHashMap.empty }
      Instances For
        Equations
        • Lean.PersistentHashSet.instInhabited = { default := Lean.PersistentHashSet.empty }
        Equations
        • Lean.PersistentHashSet.instEmptyCollection = { emptyCollection := Lean.PersistentHashSet.empty }
        @[inline]
        def Lean.PersistentHashSet.isEmpty {α : Type u_1} :
        {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet αBool
        Equations
        • s.isEmpty = s.set.isEmpty
        Instances For
          @[inline]
          def Lean.PersistentHashSet.insert {α : Type u_1} :
          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααLean.PersistentHashSet α
          Equations
          • s.insert a = { set := s.set.insert a () }
          Instances For
            @[inline]
            def Lean.PersistentHashSet.erase {α : Type u_1} :
            {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααLean.PersistentHashSet α
            Equations
            • s.erase a = { set := s.set.erase a }
            Instances For
              @[inline]
              def Lean.PersistentHashSet.find? {α : Type u_1} :
              {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααOption α
              Equations
              • s.find? a = match s.set.findEntry? a with | some (a, snd) => some a | none => none
              Instances For
                @[inline]
                def Lean.PersistentHashSet.contains {α : Type u_1} :
                {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααBool
                Equations
                • s.contains a = s.set.contains a
                Instances For
                  @[inline]
                  def Lean.PersistentHashSet.foldM {α : Type u_1} :
                  {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → {m : Type v → Type v} → [inst : Monad m] → (βαm β)βLean.PersistentHashSet αm β
                  Equations
                  Instances For
                    @[inline]
                    def Lean.PersistentHashSet.fold {α : Type u_1} :
                    {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (βαβ)βLean.PersistentHashSet αβ
                    Equations
                    Instances For