Documentation

Mathlib.Data.HashMap

Additional API for HashMap and RBSet. #

These should be replaced by proper implementations in Std.

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

The list of keys in a HashMap.

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

    The list of values in a HashMap.

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

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

      Equations
      Instances For
        def Std.RBSet.insertList {α : Type u_1} {cmp : ααOrdering} (m : Std.RBSet α cmp) (L : List α) :
        Std.RBSet α cmp

        Insert all elements of a list into an RBSet.

        Equations
        Instances For