Documentation

Mathlib.Data.HashMap

Additional API for HashMap and RBSet. #

These should be replaced by proper implementations in Batteries.

@[deprecated]
def Batteries.HashMap.keys {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (m : Batteries.HashMap α β) :
List α

The list of keys in a HashMap.

Equations
Instances For
    @[deprecated]
    def Batteries.HashMap.values {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (m : Batteries.HashMap α β) :
    List β

    The list of values in a HashMap.

    Equations
    Instances For
      @[deprecated]
      def Batteries.HashMap.consVal {α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} (self : Batteries.HashMap α (List β)) (a : α) (b : β) :

      Add a value to a HashMap α (List β) viewed as a multimap.

      Equations
      • self.consVal a b = match self.find? a with | none => self.insert a [b] | some L => self.insert a (b :: L)
      Instances For
        @[deprecated]
        def Batteries.RBSet.insertList {α : Type u_1} {cmp : ααOrdering} (m : Batteries.RBSet α cmp) (L : List α) :

        Insert all elements of a list into an RBSet.

        Equations
        Instances For