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)
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)
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.
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.
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.
Merge two PersistentHashMap
s. 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.
Merge two PersistentHashMap
s. 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.