Documentation

Batteries.Data.HashMap.Basic

A hash is lawful if elements which compare equal under == have equal hash.

  • hash_eq : ∀ {a b : α}, (a == b) = truehash a = hash b

    Two elements which compare equal under the BEq instance have equal hash.

Instances
    theorem Batteries.HashMap.LawfulHashable.hash_eq {α : Type u_1} [BEq α] [Hashable α] [self : Batteries.HashMap.LawfulHashable α] {a : α} {b : α} :
    (a == b) = truehash a = hash b

    Two elements which compare equal under the BEq instance have equal hash.

    def Batteries.HashMap.Imp.Buckets (α : Type u) (β : Type v) :
    Type (max 0 u v)

    The bucket array of a HashMap is a nonempty array of AssocLists. (This type is an internal implementation detail of HashMap.)

    Equations
    Instances For
      def Batteries.HashMap.Imp.Buckets.mk {α : Type u_1} {β : Type u_2} (buckets : optParam Nat 8) (h : autoParam (0 < buckets) _auto✝) :

      Construct a new empty bucket array with the specified capacity.

      Equations
      Instances For
        def Batteries.HashMap.Imp.Buckets.update {α : Type u_1} {β : Type u_2} (data : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (h : i.toNat < data.val.size) :

        Update one bucket in the bucket array with a new value.

        Equations
        • data.update i d h = data.val.uset i d h,
        Instances For
          noncomputable def Batteries.HashMap.Imp.Buckets.size {α : Type u_1} {β : Type u_2} (data : Batteries.HashMap.Imp.Buckets α β) :

          The number of elements in the bucket array. Note: this is marked noncomputable because it is only intended for specification.

          Equations
          Instances For
            @[simp]
            theorem Batteries.HashMap.Imp.Buckets.update_size {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (h : i.toNat < self.val.size) :
            (self.update i d h).val.size = self.val.size
            @[specialize #[]]
            def Batteries.HashMap.Imp.Buckets.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (self : Batteries.HashMap.Imp.Buckets α β) :

            Map a function over the values in the map.

            Equations
            Instances For
              structure Batteries.HashMap.Imp.Buckets.WF {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (buckets : Batteries.HashMap.Imp.Buckets α β) :

              The well-formedness invariant for the bucket array says that every element hashes to its index (assuming the hash is lawful - otherwise there are no promises about where elements are located).

              Instances For
                theorem Batteries.HashMap.Imp.Buckets.WF.distinct {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {buckets : Batteries.HashMap.Imp.Buckets α β} (self : buckets.WF) [Batteries.HashMap.LawfulHashable α] [PartialEquivBEq α] (bucket : Batteries.AssocList α β) :
                bucket buckets.val.dataList.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) bucket.toList

                The elements of a bucket are all distinct according to the BEq relation.

                theorem Batteries.HashMap.Imp.Buckets.WF.hash_self {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {buckets : Batteries.HashMap.Imp.Buckets α β} (self : buckets.WF) (i : Nat) (h : i < buckets.val.size) :
                Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % buckets.val.size).toNat = i) buckets.val[i]

                Every element in a bucket should hash to its location.

                structure Batteries.HashMap.Imp (α : Type u) (β : Type v) :
                Type (max u v)

                HashMap.Imp α β is the internal implementation type of HashMap α β.

                • size : Nat

                  The number of elements stored in the HashMap. We cache this both so that we can implement .size in O(1), and also because we use the size to determine when to resize the map.

                • The bucket array of the HashMap.

                Instances For
                  @[inline]

                  Given a desired capacity, this returns the number of buckets we should reserve. A "load factor" of 0.75 is the usual standard for hash maps, so we return capacity * 4 / 3.

                  Equations
                  Instances For
                    @[inline]
                    def Batteries.HashMap.Imp.empty' {α : Type u_1} {β : Type u_2} (buckets : optParam Nat 8) (h : autoParam (0 < buckets) _auto✝) :

                    Constructs an empty hash map with the specified nonzero number of buckets.

                    Equations
                    Instances For
                      def Batteries.HashMap.Imp.empty {α : Type u_1} {β : Type u_2} (capacity : optParam Nat 0) :

                      Constructs an empty hash map with the specified target capacity.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Batteries.HashMap.Imp.mkIdx {n : Nat} (h : 0 < n) (u : USize) :
                        { u : USize // u.toNat < n }

                        Calculates the bucket index from a hash value u.

                        Equations
                        Instances For
                          @[inline]
                          def Batteries.HashMap.Imp.reinsertAux {α : Type u_1} {β : Type u_2} [Hashable α] (data : Batteries.HashMap.Imp.Buckets α β) (a : α) (b : β) :

                          Inserts a key-value pair into the bucket array. This function assumes that the data is not already in the array, which is appropriate when reinserting elements into the array after a resize.

                          Equations
                          Instances For
                            @[inline]
                            def Batteries.HashMap.Imp.foldM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δαβm δ) (d : δ) (map : Batteries.HashMap.Imp α β) :
                            m δ

                            Folds a monadic function over the elements in the map (in arbitrary order).

                            Equations
                            Instances For
                              @[inline]
                              def Batteries.HashMap.Imp.fold {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δαβδ) (d : δ) (m : Batteries.HashMap.Imp α β) :
                              δ

                              Folds a function over the elements in the map (in arbitrary order).

                              Equations
                              Instances For
                                @[inline]
                                def Batteries.HashMap.Imp.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : αβm PUnit) (h : Batteries.HashMap.Imp α β) :

                                Runs a monadic function over the elements in the map (in arbitrary order).

                                Equations
                                Instances For
                                  def Batteries.HashMap.Imp.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) :
                                  Option (α × β)

                                  Given a key a, returns a key-value pair in the map whose key compares equal to a.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Batteries.HashMap.Imp.find? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) :

                                    Looks up an element in the map with key a.

                                    Equations
                                    Instances For
                                      def Batteries.HashMap.Imp.contains {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) :

                                      Returns true if the element a is in the map.

                                      Equations
                                      Instances For
                                        def Batteries.HashMap.Imp.expand {α : Type u_1} {β : Type u_2} [Hashable α] (size : Nat) (buckets : Batteries.HashMap.Imp.Buckets α β) :

                                        Copies all the entries from buckets into a new hash map with a larger capacity.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[irreducible]
                                          def Batteries.HashMap.Imp.expand.go {α : Type u_1} {β : Type u_2} [Hashable α] (i : Nat) (source : Array (Batteries.AssocList α β)) (target : Batteries.HashMap.Imp.Buckets α β) :

                                          Inner loop of expand. Copies elements source[i:] into target, destroying source in the process.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[inline]
                                            def Batteries.HashMap.Imp.insert {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) (b : β) :

                                            Inserts key-value pair a, b into the map. If an element equal to a is already in the map, it is replaced by b.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Batteries.HashMap.Imp.erase {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) :

                                              Removes key a from the map. If it does not exist in the map, the map is returned unchanged.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[inline]
                                                def Batteries.HashMap.Imp.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (self : Batteries.HashMap.Imp α β) :

                                                Map a function over the values in the map.

                                                Equations
                                                Instances For
                                                  def Batteries.HashMap.Imp.modify {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Batteries.HashMap.Imp α β) (a : α) (f : αββ) :

                                                  Performs an in-place edit of the value, ensuring that the value is used linearly.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[specialize #[]]
                                                    def Batteries.HashMap.Imp.filterMap {α : Type u} {β : Type v} {γ : Type w} (f : αβOption γ) (m : Batteries.HashMap.Imp α β) :

                                                    Applies f to each key-value pair a, b in the map. If it returns some c then a, c is pushed into the new map; else the key is removed from the map.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[specialize #[]]
                                                      def Batteries.HashMap.Imp.filterMap.go {α : Type u} {β : Type v} {γ : Type w} (f : αβOption γ) (acc : Batteries.AssocList α γ) :

                                                      Inner loop of filterMap. Note that this reverses the bucket lists, but this is fine since bucket lists are unordered.

                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Batteries.HashMap.Imp.filter {α : Type u_1} {β : Type u_2} (f : αβBool) (m : Batteries.HashMap.Imp α β) :

                                                        Constructs a map with the set of all pairs a, b such that f returns true.

                                                        Equations
                                                        Instances For
                                                          inductive Batteries.HashMap.Imp.WF {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} :

                                                          The well-formedness invariant for a hash map. The first constructor is the real invariant, and the others allow us to "cheat" in this file and define insert and erase, which have more complex proofs that are delayed to Batteries.Data.HashMap.Lemmas.

                                                          • mk: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Batteries.HashMap.Imp α x}, m.size = m.buckets.sizem.buckets.WFm.WF

                                                            The real well-formedness invariant:

                                                            • The size field should match the actual number of elements in the map
                                                            • The bucket array should be well-formed, meaning that if the hashable instance is lawful then every element hashes to its index.
                                                          • empty': ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {n : Nat} {h : 0 < n}, (Batteries.HashMap.Imp.empty' n h).WF

                                                            The empty hash map is well formed.

                                                          • insert: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Batteries.HashMap.Imp α x} {a : α} {b : x}, m.WF(m.insert a b).WF

                                                            Inserting into a well formed hash map yields a well formed hash map.

                                                          • erase: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Batteries.HashMap.Imp α x} {a : α}, m.WF(m.erase a).WF

                                                            Removing an element from a well formed hash map yields a well formed hash map.

                                                          • modify: ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] {x : Type u_2} {m : Batteries.HashMap.Imp α x} {a : α} {f : αxx}, m.WF(m.modify a f).WF

                                                            Replacing an element in a well formed hash map yields a well formed hash map.

                                                          Instances For
                                                            theorem Batteries.HashMap.Imp.WF.empty {α : Type u_1} {β : Type u_2} {n : Nat} [BEq α] [Hashable α] :
                                                            def Batteries.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
                                                            Type (max 0 u v)

                                                            HashMap α β is a key-value map which stores elements in an array using a hash function to find the values. This allows it to have very good performance for lookups (average O(1) for a perfectly random hash function), but it is not a persistent data structure, meaning that one should take care to use the map linearly when performing updates. Copies are O(n).

                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Batteries.mkHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (capacity : optParam Nat 0) :

                                                              Make a new hash map with the specified capacity.

                                                              Equations
                                                              Instances For
                                                                instance Batteries.HashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                                                Equations
                                                                • Batteries.HashMap.instInhabited = { default := Batteries.mkHashMap }
                                                                Equations
                                                                • Batteries.HashMap.instEmptyCollection = { emptyCollection := Batteries.mkHashMap }
                                                                @[inline]
                                                                def Batteries.HashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :

                                                                Make a new empty hash map.

                                                                (empty : Batteries.HashMap Int Int).toList = []
                                                                
                                                                Equations
                                                                • Batteries.HashMap.empty = Batteries.mkHashMap
                                                                Instances For
                                                                  @[inline]
                                                                  def Batteries.HashMap.size {α : Type u_1} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βNat

                                                                  The number of elements in the hash map.

                                                                  (ofList [("one", 1), ("two", 2)]).size = 2
                                                                  
                                                                  Equations
                                                                  • self.size = self.val.size
                                                                  Instances For
                                                                    @[inline]
                                                                    def Batteries.HashMap.isEmpty {α : Type u_1} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βBool

                                                                    Is the map empty?

                                                                    (empty : Batteries.HashMap Int Int).isEmpty = true
                                                                    (ofList [("one", 1), ("two", 2)]).isEmpty = false
                                                                    
                                                                    Equations
                                                                    Instances For
                                                                      def Batteries.HashMap.insert {α : Type u_1} :
                                                                      {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαβBatteries.HashMap α β

                                                                      Inserts key-value pair a, b into the map. If an element equal to a is already in the map, it is replaced by b.

                                                                      def hashMap := ofList [("one", 1), ("two", 2)]
                                                                      hashMap.insert "three" 3 = {"one" => 1, "two" => 2, "three" => 3}
                                                                      hashMap.insert "two" 0 = {"one" => 1, "two" => 0}
                                                                      
                                                                      Equations
                                                                      • self.insert a b = self.val.insert a b,
                                                                      Instances For
                                                                        @[inline]
                                                                        def Batteries.HashMap.insert' {α : Type u_1} :
                                                                        {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαβBatteries.HashMap α β × Bool

                                                                        Similar to insert, but also returns a boolean flag indicating whether an existing entry has been replaced with a => b.

                                                                        def hashMap := ofList [("one", 1), ("two", 2)]
                                                                        hashMap.insert' "three" 3 = ({"one" => 1, "two" => 2, "three" => 3}, false)
                                                                        hashMap.insert' "two" 0 = ({"one" => 1, "two" => 0}, true)
                                                                        
                                                                        Equations
                                                                        • m.insert' a b = let old := m.size; let m' := m.insert a b; let replaced := old == m'.size; (m', replaced)
                                                                        Instances For
                                                                          @[inline]
                                                                          def Batteries.HashMap.erase {α : Type u_1} :
                                                                          {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαBatteries.HashMap α β

                                                                          Removes key a from the map. If it does not exist in the map, the map is returned unchanged.

                                                                          def hashMap := ofList [("one", 1), ("two", 2)]
                                                                          hashMap.erase "one" = {"two" => 2}
                                                                          hashMap.erase "three" = {"one" => 1, "two" => 2}
                                                                          
                                                                          Equations
                                                                          • self.erase a = self.val.erase a,
                                                                          Instances For
                                                                            def Batteries.HashMap.modify {α : Type u_1} :
                                                                            {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βα(αββ)Batteries.HashMap α β

                                                                            Performs an in-place edit of the value, ensuring that the value is used linearly. The function f is passed the original key of the entry, along with the value in the map.

                                                                            (ofList [("one", 1), ("two", 2)]).modify "one" (fun _ v => v + 1) = {"one" => 2, "two" => 2}
                                                                            (ofList [("one", 1), ("two", 2)]).modify "three" (fun _ v => v + 1) = {"one" => 1, "two" => 2}
                                                                            
                                                                            Equations
                                                                            • self.modify a f = self.val.modify a f,
                                                                            Instances For
                                                                              @[inline]
                                                                              def Batteries.HashMap.findEntry? {α : Type u_1} :
                                                                              {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαOption (α × β)

                                                                              Given a key a, returns a key-value pair in the map whose key compares equal to a. Note that the returned key may not be identical to the input, if == ignores some part of the value.

                                                                              def hashMap := ofList [("one", 1), ("two", 2)]
                                                                              hashMap.findEntry? "one" = some ("one", 1)
                                                                              hashMap.findEntry? "three" = none
                                                                              
                                                                              Equations
                                                                              • self.findEntry? a = self.val.findEntry? a
                                                                              Instances For
                                                                                @[inline]
                                                                                def Batteries.HashMap.find? {α : Type u_1} :
                                                                                {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαOption β

                                                                                Looks up an element in the map with key a.

                                                                                def hashMap := ofList [("one", 1), ("two", 2)]
                                                                                hashMap.find? "one" = some 1
                                                                                hashMap.find? "three" = none
                                                                                
                                                                                Equations
                                                                                • self.find? a = self.val.find? a
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Batteries.HashMap.findD {α : Type u_1} :
                                                                                  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαββ

                                                                                  Looks up an element in the map with key a. Returns b₀ if the element is not found.

                                                                                  def hashMap := ofList [("one", 1), ("two", 2)]
                                                                                  hashMap.findD "one" 0 = 1
                                                                                  hashMap.findD "three" 0 = 0
                                                                                  
                                                                                  Equations
                                                                                  • self.findD a b₀ = (self.find? a).getD b₀
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Batteries.HashMap.find! {α : Type u_1} :
                                                                                    {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → [inst : Inhabited β] → Batteries.HashMap α βαβ

                                                                                    Looks up an element in the map with key a. Panics if the element is not found.

                                                                                    def hashMap := ofList [("one", 1), ("two", 2)]
                                                                                    hashMap.find! "one" = 1
                                                                                    hashMap.find! "three" => panic!
                                                                                    
                                                                                    Equations
                                                                                    • self.find! a = (self.find? a).getD (panicWithPosWithDecl "Batteries.Data.HashMap.Basic" "Batteries.HashMap.find!" 380 23 "key is not in the map")
                                                                                    Instances For
                                                                                      instance Batteries.HashMap.instGetElemOptionTrue {α : Type u_1} :
                                                                                      {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → GetElem (Batteries.HashMap α β) α (Option β) fun (x : Batteries.HashMap α β) (x : α) => True
                                                                                      Equations
                                                                                      • Batteries.HashMap.instGetElemOptionTrue = { getElem := fun (m : Batteries.HashMap α β) (k : α) (x_1 : True) => m.find? k }
                                                                                      @[inline]
                                                                                      def Batteries.HashMap.contains {α : Type u_1} :
                                                                                      {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βαBool

                                                                                      Returns true if the element a is in the map.

                                                                                      def hashMap := ofList [("one", 1), ("two", 2)]
                                                                                      hashMap.contains "one" = true
                                                                                      hashMap.contains "three" = false
                                                                                      
                                                                                      Equations
                                                                                      • self.contains a = self.val.contains a
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def Batteries.HashMap.foldM {α : Type u_1} :
                                                                                        {x : BEq α} → {x_1 : Hashable α} → {m : Type u_2 → Type u_3} → {δ : Type u_2} → {β : Type u_4} → [inst : Monad m] → (δαβm δ)δBatteries.HashMap α βm δ

                                                                                        Folds a monadic function over the elements in the map (in arbitrary order).

                                                                                        def sumEven (sum: Nat) (k : String) (v : Nat) : Except String Nat :=
                                                                                          if v % 2 == 0 then pure (sum + v) else throw s!"value {v} at key {k} is not even"
                                                                                        
                                                                                        foldM sumEven 0 (ofList [("one", 1), ("three", 3)]) =
                                                                                          Except.error "value 3 at key three is not even"
                                                                                        foldM sumEven 0 (ofList [("two", 2), ("four", 4)]) = Except.ok 6
                                                                                        
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Batteries.HashMap.fold {α : Type u_1} :
                                                                                          {x : BEq α} → {x_1 : Hashable α} → {δ : Type u_2} → {β : Type u_3} → (δαβδ)δBatteries.HashMap α βδ

                                                                                          Folds a function over the elements in the map (in arbitrary order).

                                                                                          fold (fun sum _ v => sum + v) 0 (ofList [("one", 1), ("two", 2)]) = 3
                                                                                          
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            def Batteries.HashMap.mergeWithM {α : Type u_1} :
                                                                                            {x : BEq α} → {x_1 : Hashable α} → {m : Type (max u_2 u_1) → Type u_3} → {β : Type (max u_2 u_1)} → [inst : Monad m] → (αββm β)Batteries.HashMap α βBatteries.HashMap α βm (Batteries.HashMap α β)

                                                                                            Combines two hashmaps using a monadic function f to combine two values at a key.

                                                                                            def map1 := ofList [("one", 1), ("two", 2)]
                                                                                            def map2 := ofList [("two", 2), ("three", 3)]
                                                                                            def map3 := ofList [("two", 3), ("three", 3)]
                                                                                            def mergeIfNoConflict? (_ : String) (v₁ v₂ : Nat) : Option Nat :=
                                                                                              if v₁ != v₂ then none else some v₁
                                                                                            
                                                                                            
                                                                                            mergeWithM mergeIfNoConflict? map1 map2 = some {"one" => 1, "two" => 2, "three" => 3}
                                                                                            mergeWithM mergeIfNoConflict? map1 map3 = none
                                                                                            
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Batteries.HashMap.mergeWith {α : Type u_1} :
                                                                                              {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → (αβββ)Batteries.HashMap α βBatteries.HashMap α βBatteries.HashMap α β

                                                                                              Combines two hashmaps using function f to combine two values at a key.

                                                                                              mergeWith (fun _ v₁ v₂ => v₁ + v₂ )
                                                                                                (ofList [("one", 1), ("two", 2)]) (ofList [("two", 2), ("three", 3)]) =
                                                                                                  {"one" => 1, "two" => 4, "three" => 3}
                                                                                              
                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                def Batteries.HashMap.forM {α : Type u_1} :
                                                                                                {x : BEq α} → {x_1 : Hashable α} → {m : Type u_2 → Type u_3} → {β : Type u_4} → [inst : Monad m] → (αβm PUnit)Batteries.HashMap α βm PUnit

                                                                                                Runs a monadic function over the elements in the map (in arbitrary order).

                                                                                                def checkEven (k : String) (v : Nat) : Except String Unit :=
                                                                                                  if v % 2 == 0 then pure () else throw s!"value {v} at key {k} is not even"
                                                                                                
                                                                                                forM checkEven (ofList [("one", 1), ("three", 3)]) = Except.error "value 3 at key three is not even"
                                                                                                forM checkEven (ofList [("two", 2), ("four", 4)]) = Except.ok ()
                                                                                                
                                                                                                Equations
                                                                                                Instances For
                                                                                                  def Batteries.HashMap.toList {α : Type u_1} :
                                                                                                  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βList (α × β)

                                                                                                  Converts the map into a list of key-value pairs.

                                                                                                  open List
                                                                                                  (ofList [("one", 1), ("two", 2)]).toList ~ [("one", 1), ("two", 2)]
                                                                                                  
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def Batteries.HashMap.toArray {α : Type u_1} :
                                                                                                    {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βArray (α × β)

                                                                                                    Converts the map into an array of key-value pairs.

                                                                                                    open List
                                                                                                    (ofList [("one", 1), ("two", 2)]).toArray.data ~ #[("one", 1), ("two", 2)].data
                                                                                                    
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def Batteries.HashMap.numBuckets {α : Type u_1} :
                                                                                                      {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α βNat

                                                                                                      The number of buckets in the hash map.

                                                                                                      Equations
                                                                                                      • self.numBuckets = self.val.buckets.val.size
                                                                                                      Instances For
                                                                                                        def Batteries.HashMap.ofList {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) :

                                                                                                        Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

                                                                                                        ofList [("one", 1), ("one", 2)] = {"one" => 2}
                                                                                                        
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def Batteries.HashMap.ofListWith {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (l : List (α × β)) (f : βββ) :

                                                                                                          Variant of ofList which accepts a function that combines values of duplicated keys.

                                                                                                          ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}
                                                                                                          
                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For