ink

def Lean.PersistentHashMap.insert' {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (m : Lean.PersistentHashMap α β) (a : α) (b : β) : Lean.PersistentHashMap α β × Bool

Similar to insert, but also returns a Boolean flag indicating whether an existing entry has been replaced with a ↦ b↦ b.

Equations

• Lean.PersistentHashMap.insert' m a b = let oldSize := m.size; let m := Lean.PersistentHashMap.insert m a b; (m, m.size == oldSize)

ink

def Lean.PersistentHashMap.toArray {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (m : Lean.PersistentHashMap α β) : Array (α × β)

Turns a PersistentHashMap into an array of key-value pairs.

Equations

• Lean.PersistentHashMap.toArray m = Lean.PersistentHashMap.foldl m (fun xs k v => Array.push xs (k, v)) (Array.mkEmpty m.size)

ink

def Lean.PersistentHashMap.ofList {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (xs : List (α × β)) : Lean.PersistentHashMap α β

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.

ink

def Lean.PersistentHashMap.ofListWith {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (xs : List (α × β)) (f : α → β → β → β) : Lean.PersistentHashMap α β

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.

ink

def Lean.PersistentHashMap.ofArray {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (xs : Array (α × β)) : Lean.PersistentHashMap α β

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.

ink

def Lean.PersistentHashMap.ofArrayWith {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (xs : Array (α × β)) (f : α → β → β → β) : Lean.PersistentHashMap α β

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.

ink

@[specialize #[]]

def Lean.PersistentHashMap.mergeWithM {α : Type u_1} [inst : BEq α] [inst : Hashable α] {m : Type (maxu_2u_1) → Type u_3} {β : Type (maxu_2u_1)} [inst : Monad m] (self : Lean.PersistentHashMap α β) (other : Lean.PersistentHashMap α β) (f : α → β → β → m β) : m (Lean.PersistentHashMap α β)

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.

ink

@[inline]

def Lean.PersistentHashMap.mergeWith {α : Type u_1} [inst : BEq α] [inst : Hashable α] {β : Type u_2} (self : Lean.PersistentHashMap α β) (other : Lean.PersistentHashMap α β) (f : α → β → β → β) : Lean.PersistentHashMap α β

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.