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

• Std.HashMap.keys m = Std.HashMap.fold (fun (ks : List α) (k : α) (x : β) => k :: ks) [] m

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

The list of values in a HashMap.

Equations

• Std.HashMap.values m = Std.HashMap.fold (fun (vs : List β) (x : α) (v : β) => v :: vs) [] m

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

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

Equations

• Std.HashMap.consVal self a b = match Std.HashMap.find? self a with | none => Std.HashMap.insert self a [b] | some L => Std.HashMap.insert self a (b :: L)

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

• Std.RBSet.insertList m L = List.foldl (fun (m : Std.RBSet α cmp) (a : α) => Std.RBSet.insert m a) m L