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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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 : Lean.PersistentHashMap α β) (other : Lean.PersistentHashMap α β) (f : αββm β) :

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]
            def Lean.PersistentHashMap.mergeWith {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (self : Lean.PersistentHashMap α β) (other : Lean.PersistentHashMap α β) (f : αβββ) :

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For