Additional API for HashMap and RBSet.

These should be replaced by proper implementations in Batteries.

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

The list of keys in a HashMap.

Equations

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

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

The list of values in a HashMap.

Equations

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

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

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)

def Batteries.RBSet.insertList {α : Type u_1} {cmp : α → α → Ordering} (m : Batteries.RBSet α cmp) (L : List α) : Batteries.RBSet α cmp

Insert all elements of a list into an RBSet.

Equations

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