Documentation

Lean.Data.HashSet

def Lean.HashSetBucket (α : Type u) :
Type (max 0 u)
Equations
Instances For
    def Lean.HashSetBucket.update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
    Equations
    • data.update i d h = data.val.uset i d h,
    Instances For
      @[simp]
      theorem Lean.HashSetBucket.size_update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
      (data.update i d h).val.size = data.val.size
      @[deprecated Std.HashSet.Raw]
      structure Lean.HashSetImp (α : Type u) :
      Instances For
        @[deprecated Std.HashSet.Raw.empty]
        def Lean.mkHashSetImp {α : Type u} (capacity : optParam Nat 8) :
        Equations
        Instances For
          @[inline]
          def Lean.HashSetImp.reinsertAux {α : Type u} (hashFn : αUInt64) (data : Lean.HashSetBucket α) (a : α) :
          Equations
          Instances For
            @[inline]
            def Lean.HashSetImp.foldBucketsM {α : Type u} {δ : Type w} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (d : δ) (f : δαm δ) :
            m δ
            Equations
            Instances For
              @[inline]
              def Lean.HashSetImp.foldBuckets {α : Type u} {δ : Type w} (data : Lean.HashSetBucket α) (d : δ) (f : δαδ) :
              δ
              Equations
              Instances For
                @[inline]
                def Lean.HashSetImp.foldM {α : Type u} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαm δ) (d : δ) (h : Lean.HashSetImp α) :
                m δ
                Equations
                Instances For
                  @[inline]
                  def Lean.HashSetImp.fold {α : Type u} {δ : Type w} (f : δαδ) (d : δ) (m : Lean.HashSetImp α) :
                  δ
                  Equations
                  Instances For
                    @[inline]
                    def Lean.HashSetImp.forBucketsM {α : Type u} {m : Type w → Type w} [Monad m] (data : Lean.HashSetBucket α) (f : αm PUnit) :
                    Equations
                    Instances For
                      @[inline]
                      def Lean.HashSetImp.forM {α : Type u} {m : Type w → Type w} [Monad m] (f : αm PUnit) (h : Lean.HashSetImp α) :
                      Equations
                      Instances For
                        def Lean.HashSetImp.find? {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
                        Equations
                        Instances For
                          def Lean.HashSetImp.contains {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
                          Equations
                          • { size := size, buckets := buckets }.contains a = match Lean.HashSetImp.mkIdx (hash a) with | i, h => buckets.val[i].contains a
                          Instances For
                            @[irreducible]
                            def Lean.HashSetImp.moveEntries {α : Type u} [Hashable α] (i : Nat) (source : Array (List α)) (target : Lean.HashSetBucket α) :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Lean.HashSetImp.expand {α : Type u} [Hashable α] (size : Nat) (buckets : Lean.HashSetBucket α) :
                              Equations
                              Instances For
                                def Lean.HashSetImp.insert {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Lean.HashSetImp.erase {α : Type u} [BEq α] [Hashable α] (m : Lean.HashSetImp α) (a : α) :
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    inductive Lean.HashSetImp.WellFormed {α : Type u} [BEq α] [Hashable α] :
                                    Instances For
                                      @[deprecated Std.HashSet]
                                      def Lean.HashSet (α : Type u) [BEq α] [Hashable α] :
                                      Type (max 0 u)
                                      Equations
                                      Instances For
                                        @[deprecated Std.HashSet.empty]
                                        def Lean.mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity : optParam Nat 8) :
                                        Equations
                                        Instances For
                                          @[inline, deprecated Std.HashSet.empty]
                                          def Lean.HashSet.empty {α : Type u_1} [BEq α] [Hashable α] :
                                          Equations
                                          • Lean.HashSet.empty = Lean.mkHashSet
                                          Instances For
                                            Equations
                                            • Lean.HashSet.instInhabited = { default := Lean.mkHashSet }
                                            Equations
                                            • Lean.HashSet.instEmptyCollection = { emptyCollection := Lean.mkHashSet }
                                            @[inline]
                                            def Lean.HashSet.insert {α : Type u} :
                                            {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet ααLean.HashSet α
                                            Equations
                                            Instances For
                                              @[inline]
                                              def Lean.HashSet.erase {α : Type u} :
                                              {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet ααLean.HashSet α
                                              Equations
                                              Instances For
                                                @[inline]
                                                def Lean.HashSet.find? {α : Type u} :
                                                {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet ααOption α
                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Lean.HashSet.contains {α : Type u} :
                                                  {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet ααBool
                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Lean.HashSet.foldM {α : Type u} :
                                                    {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → {m : Type w → Type w} → [inst : Monad m] → (δαm δ)δLean.HashSet αm δ
                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lean.HashSet.fold {α : Type u} :
                                                      {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δαδ)δLean.HashSet αδ
                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Lean.HashSet.forM {α : Type u} :
                                                        {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → Lean.HashSet α(αm PUnit)m PUnit
                                                        Equations
                                                        Instances For
                                                          instance Lean.HashSet.instForM {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → {m : Type u_1 → Type u_1} → ForM m (Lean.HashSet α) α
                                                          Equations
                                                          • Lean.HashSet.instForM = { forM := fun [Monad m] => Lean.HashSet.forM }
                                                          instance Lean.HashSet.instForIn {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → {m : Type (max u_1 u_2) → Type u_1} → ForIn m (Lean.HashSet α) α
                                                          Equations
                                                          • Lean.HashSet.instForIn = { forIn := fun {β : Type (max ?u.34 ?u.33)} [Monad m] => ForM.forIn }
                                                          @[inline]
                                                          def Lean.HashSet.size {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αNat
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Lean.HashSet.isEmpty {α : Type u} :
                                                            {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αBool
                                                            Equations
                                                            Instances For
                                                              def Lean.HashSet.toList {α : Type u} :
                                                              {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αList α
                                                              Equations
                                                              Instances For
                                                                def Lean.HashSet.toArray {α : Type u} :
                                                                {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αArray α
                                                                Equations
                                                                Instances For
                                                                  def Lean.HashSet.numBuckets {α : Type u} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αNat
                                                                  Equations
                                                                  • m.numBuckets = m.val.buckets.val.size
                                                                  Instances For
                                                                    def Lean.HashSet.insertMany {α : Type u} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → {ρ : Type u_1} → [inst : ForIn Id ρ α] → Lean.HashSet αρLean.HashSet α

                                                                    Insert many elements into a HashSet.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[inline]
                                                                      def Lean.HashSet.merge {α : Type u} [BEq α] [Hashable α] (s : Lean.HashSet α) (t : Lean.HashSet α) :

                                                                      O(|t|) amortized. Merge two HashSets.

                                                                      Equations
                                                                      Instances For