Documentation

Batteries.Lean.PersistentHashMap

def Lean.PersistentHashMap.ofList {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (xs : List (α × β)) :

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

Equations
    Instances For
      def Lean.PersistentHashMap.ofListWith {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (xs : List (α × β)) (f : αβββ) :

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

      Equations
        Instances For
          def Lean.PersistentHashMap.ofArray {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (xs : Array (α × β)) :

          Builds a PersistentHashMap from an array of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

          Equations
            Instances For
              def Lean.PersistentHashMap.ofArrayWith {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (xs : Array (α × β)) (f : αβββ) :

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

              Equations
                Instances For
                  @[specialize #[]]
                  def Lean.PersistentHashMap.mergeWithM {α : Type u_1} [BEq α] [Hashable α] {m : Type (max u_2 u_1) → Type u_3} {β : Type (max u_2 u_1)} [Monad m] (self other : PersistentHashMap α β) (f : αββm β) :

                  Merge two PersistentHashMaps. The values of keys which appear in both maps are combined using the monadic function f.

                  Equations
                    Instances For
                      @[inline]
                      def Lean.PersistentHashMap.mergeWith {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (self other : PersistentHashMap α β) (f : αβββ) :

                      Merge two PersistentHashMaps. The values of keys which appear in both maps are combined using f.

                      Equations
                        Instances For