Documentation

Lean.Data.PersistentHashSet

structure Lean.PersistentHashSet (α : Type u) [BEq α] [Hashable α] :
Instances For
    @[inline, reducible]
    abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] :
    Equations
    Instances For
      @[inline]
      Equations
      • Lean.PersistentHashSet.empty = { set := Lean.PersistentHashMap.empty }
      Instances For
        Equations
        • Lean.PersistentHashSet.instInhabitedPersistentHashSet = { default := Lean.PersistentHashSet.empty }
        Equations
        • Lean.PersistentHashSet.instEmptyCollectionPersistentHashSet = { emptyCollection := Lean.PersistentHashSet.empty }
        @[inline]
        def Lean.PersistentHashSet.isEmpty {α : Type u_1} :
        {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet αBool
        Equations
        Instances For
          @[inline]
          def Lean.PersistentHashSet.insert {α : Type u_1} :
          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααLean.PersistentHashSet α
          Equations
          Instances For
            @[inline]
            def Lean.PersistentHashSet.erase {α : Type u_1} :
            {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααLean.PersistentHashSet α
            Equations
            Instances For
              @[inline]
              def Lean.PersistentHashSet.find? {α : Type u_1} :
              {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααOption α
              Equations
              Instances For
                @[inline]
                def Lean.PersistentHashSet.contains {α : Type u_1} :
                {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet ααBool
                Equations
                Instances For
                  @[inline]
                  def Lean.PersistentHashSet.size {α : Type u_1} :
                  {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet αNat
                  Equations
                  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