Documentation

Lean.Data.HashSet

def Lean.HashSetBucket (α : Type u) :
Equations
Instances For
    def Lean.HashSetBucket.update {α : Type u} (data : Lean.HashSetBucket α) (i : USize) (d : List α) (h : USize.toNat i < Array.size data.val) :
    Equations
    Instances For
      structure Lean.HashSetImp (α : Type u) :
      Instances For
        def Lean.mkHashSetImp {α : Type u} (capacity : optParam Nat 8) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]
          def Lean.HashSetImp.reinsertAux {α : Type u} (hashFn : αUInt64) (data : Lean.HashSetBucket α) (a : α) :
          Equations
          • One or more equations did not get rendered due to their size.
          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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lean.HashSetImp.contains {α : 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.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
                              • One or more equations did not get rendered due to their size.
                              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
                                      def Lean.HashSet (α : Type u) [BEq α] [Hashable α] :
                                      Equations
                                      Instances For
                                        def Lean.mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity : optParam Nat 8) :
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Lean.HashSet.empty {α : Type u_1} [BEq α] [Hashable α] :
                                          Equations
                                          • Lean.HashSet.empty = Lean.mkHashSet
                                          Instances For
                                            Equations
                                            • Lean.HashSet.instInhabitedHashSet = { default := Lean.mkHashSet }
                                            Equations
                                            • Lean.HashSet.instEmptyCollectionHashSet = { 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.instForMHashSet {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → {m : Type u_1 → Type u_1} → ForM m (Lean.HashSet α) α
                                                          Equations
                                                          • Lean.HashSet.instForMHashSet = { forM := fun [Monad m] => Lean.HashSet.forM }
                                                          instance Lean.HashSet.instForInHashSet {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → {m : Type (max u_1 u_2) → Type u_1} → ForIn m (Lean.HashSet α) α
                                                          Equations
                                                          • Lean.HashSet.instForInHashSet = { forIn := fun {β} [Monad m] => ForM.forIn }
                                                          @[inline]
                                                          def Lean.HashSet.size {α : Type u} :
                                                          {x : BEq α} → {x_1 : Hashable α} → Lean.HashSet αNat
                                                          Equations
                                                          • Lean.HashSet.size m = match m with | { val := { size := sz, buckets := buckets }, property := property } => sz
                                                          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
                                                                  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