Documentation

Std.Data.DHashMap.Raw

The type DHashMap.Raw itself is defined in the module Std.Data.DHashmap.RawDef for import structure reasons.

@[inline]
def Std.DHashMap.Raw.empty {α : Type u} {β : αType v} (capacity : optParam Nat 8) :

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations and {} to create an empty hash map with the default capacity.

Equations
Instances For
    Equations
    • Std.DHashMap.Raw.instEmptyCollection = { emptyCollection := Std.DHashMap.Raw.empty }
    instance Std.DHashMap.Raw.instInhabited {α : Type u} {β : αType v} :
    Equations
    • Std.DHashMap.Raw.instInhabited = { default := }
    @[inline]
    def Std.DHashMap.Raw.insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a) :

    Inserts the given mapping into the map, replacing an existing mapping for the key if there is one.

    Equations
    Instances For
      @[inline]
      def Std.DHashMap.Raw.insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a) :

      If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

      Equations
      Instances For
        @[inline]
        def Std.DHashMap.Raw.containsThenInsert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a) :

        Checks whether a key is present in a map, and unconditionally inserts a value for the key.

        Equivalent to (but potentially faster than) calling contains followed by insert.

        Equations
        Instances For
          @[inline]
          def Std.DHashMap.Raw.getThenInsertIfNew? {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a) :

          Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

          If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

          Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

          Uses the LawfulBEq instance to cast the retrieved value to the correct type.

          Equations
          Instances For
            @[inline]
            def Std.DHashMap.Raw.containsThenInsertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a) :

            Checks whether a key is present in a map and inserts a value for the key if it was not found.

            If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

            Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              def Std.DHashMap.Raw.get? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) :
              Option (β a)

              Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

              Uses the LawfulBEq instance to cast the retrieved value to the correct type.

              Equations
              Instances For
                @[inline]
                def Std.DHashMap.Raw.contains {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) :

                Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

                Observe that this is different behavior than for lists: for lists, uses = and contains uses == for comparisons, while for hash maps, both use ==.

                Equations
                Instances For
                  instance Std.DHashMap.Raw.instMembershipOfBEqOfHashable {α : Type u} {β : αType v} [BEq α] [Hashable α] :
                  Equations
                  • Std.DHashMap.Raw.instMembershipOfBEqOfHashable = { mem := fun (a : α) (m : Std.DHashMap.Raw α β) => m.contains a = true }
                  instance Std.DHashMap.Raw.instDecidableMem {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} :
                  Equations
                  @[inline]
                  def Std.DHashMap.Raw.get {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (h : a m) :
                  β a

                  Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

                  Uses the LawfulBEq instance to cast the retrieved value to the correct type.

                  Equations
                  Instances For
                    @[inline]
                    def Std.DHashMap.Raw.getD {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) :
                    β a

                    Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

                    Uses the LawfulBEq instance to cast the retrieved value to the correct type.

                    Equations
                    Instances For
                      @[inline]
                      def Std.DHashMap.Raw.get! {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) [Inhabited (β a)] :
                      β a

                      Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

                      Uses the LawfulBEq instance to cast the retrieved value to the correct type.

                      Equations
                      Instances For
                        @[inline]
                        def Std.DHashMap.Raw.erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) (a : α) :

                        Removes the mapping for the given key if it exists.

                        Equations
                        Instances For
                          @[inline]
                          def Std.DHashMap.Raw.Const.get? {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun (x : α) => β) (a : α) :

                          Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

                          Equations
                          Instances For
                            @[inline]
                            def Std.DHashMap.Raw.Const.get {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun (x : α) => β) (a : α) (h : a m) :
                            β

                            Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

                            Equations
                            Instances For
                              @[inline]
                              def Std.DHashMap.Raw.Const.getD {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun (x : α) => β) (a : α) (fallback : β) :
                              β

                              Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

                              Equations
                              Instances For
                                @[inline]
                                def Std.DHashMap.Raw.Const.get! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : Std.DHashMap.Raw α fun (x : α) => β) (a : α) :
                                β

                                Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

                                Equations
                                Instances For
                                  @[inline]
                                  def Std.DHashMap.Raw.Const.getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun (x : α) => β) (a : α) (b : β) :
                                  Option β × Std.DHashMap.Raw α fun (x : α) => β

                                  Equivalent to (but potentially faster than) calling Const.get? followed by insertIfNew.

                                  Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

                                  If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[inline]
                                    def Std.DHashMap.Raw.isEmpty {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :

                                    Returns true if the hash map contains no mappings.

                                    Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

                                    Equations
                                    • m.isEmpty = (m.size == 0)
                                    Instances For

                                      We currently do not provide lemmas for the functions below.

                                      @[inline]
                                      def Std.DHashMap.Raw.filterMap {α : Type u} {β : αType v} {γ : αType w} (f : (a : α) → β aOption (γ a)) (m : Std.DHashMap.Raw α β) :

                                      Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

                                      Equations
                                      Instances For
                                        @[inline]
                                        def Std.DHashMap.Raw.map {α : Type u} {β : αType v} {γ : αType w} (f : (a : α) → β aγ a) (m : Std.DHashMap.Raw α β) :

                                        Updates the values of the hash map by applying the given function to all mappings.

                                        Equations
                                        Instances For
                                          @[inline]
                                          def Std.DHashMap.Raw.filter {α : Type u} {β : αType v} (f : (a : α) → β aBool) (m : Std.DHashMap.Raw α β) :

                                          Removes all mappings of the hash map for which the given function returns false.

                                          Equations
                                          Instances For
                                            @[inline]
                                            def Std.DHashMap.Raw.foldM {α : Type u} {β : αType v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ(a : α) → β am δ) (init : δ) (b : Std.DHashMap.Raw α β) :
                                            m δ

                                            Monadically computes a value by folding the given function over the mappings in the hash map in some order.

                                            Equations
                                            Instances For
                                              @[inline]
                                              def Std.DHashMap.Raw.fold {α : Type u} {β : αType v} {δ : Type w} (f : δ(a : α) → β aδ) (init : δ) (b : Std.DHashMap.Raw α β) :
                                              δ

                                              Folds the given function over the mappings in the hash map in some order.

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Std.DHashMap.Raw.forM {α : Type u} {β : αType v} {m : Type w → Type w} [Monad m] (f : (a : α) → β am PUnit) (b : Std.DHashMap.Raw α β) :

                                                Carries out a monadic action on each mapping in the hash map in some order.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Std.DHashMap.Raw.forIn {α : Type u} {β : αType v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : (a : α) → β aδm (ForInStep δ)) (init : δ) (b : Std.DHashMap.Raw α β) :
                                                  m δ

                                                  Support for the for loop construct in do blocks.

                                                  Equations
                                                  Instances For
                                                    instance Std.DHashMap.Raw.instForMSigma {α : Type u} {β : αType v} {m : Type w → Type w} :
                                                    ForM m (Std.DHashMap.Raw α β) ((a : α) × β a)
                                                    Equations
                                                    instance Std.DHashMap.Raw.instForInSigma {α : Type u} {β : αType v} {m : Type w → Type w} :
                                                    ForIn m (Std.DHashMap.Raw α β) ((a : α) × β a)
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    @[inline]
                                                    def Std.DHashMap.Raw.toList {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :
                                                    List ((a : α) × β a)

                                                    Transforms the hash map into a list of mappings in some order.

                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def Std.DHashMap.Raw.toArray {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :
                                                      Array ((a : α) × β a)

                                                      Transforms the hash map into an array of mappings in some order.

                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Std.DHashMap.Raw.Const.toList {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun (x : α) => β) :
                                                        List (α × β)

                                                        Transforms the hash map into a list of mappings in some order.

                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          def Std.DHashMap.Raw.Const.toArray {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun (x : α) => β) :
                                                          Array (α × β)

                                                          Transforms the hash map into an array of mappings in some order.

                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Std.DHashMap.Raw.keys {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :
                                                            List α

                                                            Returns a list of all keys present in the hash map in some order.

                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Std.DHashMap.Raw.keysArray {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :

                                                              Returns an array of all keys present in the hash map in some order.

                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def Std.DHashMap.Raw.values {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun (x : α) => β) :
                                                                List β

                                                                Returns a list of all values present in the hash map in some order.

                                                                Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Std.DHashMap.Raw.valuesArray {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun (x : α) => β) :

                                                                  Returns an array of all values present in the hash map in some order.

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]
                                                                    def Std.DHashMap.Raw.insertMany {α : Type u} {β : αType v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (m : Std.DHashMap.Raw α β) (l : ρ) :

                                                                    Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precendence.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      def Std.DHashMap.Raw.Const.insertMany {α : Type u} {β : Type v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ (α × β)] (m : Std.DHashMap.Raw α fun (x : α) => β) (l : ρ) :
                                                                      Std.DHashMap.Raw α fun (x : α) => β

                                                                      Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precendence.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        def Std.DHashMap.Raw.Const.insertManyUnit {α : Type u} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] (m : Std.DHashMap.Raw α fun (x : α) => Unit) (l : ρ) :
                                                                        Std.DHashMap.Raw α fun (x : α) => Unit

                                                                        Inserts multiple keys with the value () into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

                                                                        This is mainly useful to implement HashSet.insertMany, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Std.DHashMap.Raw.ofList {α : Type u} {β : αType v} [BEq α] [Hashable α] (l : List ((a : α) × β a)) :

                                                                          Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Std.DHashMap.Raw.Const.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :
                                                                            Std.DHashMap.Raw α fun (x : α) => β

                                                                            Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Std.DHashMap.Raw.Const.unitOfList {α : Type u} [BEq α] [Hashable α] (l : List α) :
                                                                              Std.DHashMap.Raw α fun (x : α) => Unit

                                                                              Creates a hash map from a list of keys, associating the value () with each key.

                                                                              This is mainly useful to implement HashSet.ofList, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

                                                                              Equations
                                                                              Instances For
                                                                                def Std.DHashMap.Raw.Internal.numBuckets {α : Type u} {β : αType v} (m : Std.DHashMap.Raw α β) :

                                                                                Returns the number of buckets in the internal representation of the hash map. This function may be useful for things like monitoring system health, but it should be considered an internal implementation detail.

                                                                                Equations
                                                                                Instances For
                                                                                  instance Std.DHashMap.Raw.instRepr {α : Type u} {β : αType v} [Repr α] [(a : α) → Repr (β a)] :
                                                                                  Equations
                                                                                  inductive Std.DHashMap.Raw.WF {α : Type u} {β : αType v} [BEq α] [Hashable α] :

                                                                                  Well-formedness predicate for hash maps. Users of DHashMap will not need to interact with this. Users of DHashMap.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that map operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

                                                                                  Instances For
                                                                                    theorem Std.DHashMap.Raw.WF.size_buckets_pos {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α β) :
                                                                                    m.WF0 < m.buckets.size

                                                                                    Internal implementation detail of the hash map

                                                                                    @[simp]
                                                                                    theorem Std.DHashMap.Raw.WF.empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {c : Nat} :
                                                                                    @[simp]
                                                                                    theorem Std.DHashMap.Raw.WF.emptyc {α : Type u} {β : αType v} [BEq α] [Hashable α] :
                                                                                    .WF
                                                                                    theorem Std.DHashMap.Raw.WF.insert {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a} (h : m.WF) :
                                                                                    (m.insert a b).WF
                                                                                    theorem Std.DHashMap.Raw.WF.containsThenInsert {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a} (h : m.WF) :
                                                                                    (m.containsThenInsert a b).snd.WF
                                                                                    theorem Std.DHashMap.Raw.WF.containsThenInsertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a} (h : m.WF) :
                                                                                    (m.containsThenInsertIfNew a b).snd.WF
                                                                                    theorem Std.DHashMap.Raw.WF.erase {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} (h : m.WF) :
                                                                                    (m.erase a).WF
                                                                                    theorem Std.DHashMap.Raw.WF.insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a} (h : m.WF) :
                                                                                    (m.insertIfNew a b).WF
                                                                                    theorem Std.DHashMap.Raw.WF.getThenInsertIfNew? {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a} (h : m.WF) :
                                                                                    (m.getThenInsertIfNew? a b).snd.WF
                                                                                    theorem Std.DHashMap.Raw.WF.filter {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} {f : (a : α) → β aBool} (h : m.WF) :
                                                                                    theorem Std.DHashMap.Raw.WF.Const.getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun (x : α) => β} {a : α} {b : β} (h : m.WF) :
                                                                                    theorem Std.DHashMap.Raw.WF.insertMany {α : Type u} {β : αType v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Raw α β} {l : ρ} (h : m.WF) :
                                                                                    (m.insertMany l).WF
                                                                                    theorem Std.DHashMap.Raw.WF.Const.insertMany {α : Type u} {β : Type v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ (α × β)] {m : Std.DHashMap.Raw α fun (x : α) => β} {l : ρ} (h : m.WF) :
                                                                                    theorem Std.DHashMap.Raw.WF.Const.insertManyUnit {α : Type u} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] {m : Std.DHashMap.Raw α fun (x : α) => Unit} {l : ρ} (h : m.WF) :
                                                                                    theorem Std.DHashMap.Raw.WF.ofList {α : Type u} {β : αType v} [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
                                                                                    theorem Std.DHashMap.Raw.WF.Const.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] {l : List (α × β)} :