inductive Lean.PersistentHashMap.Entry (α : Type u) (β : Type v) (σ : Type w) : Type (max (max u v) w)

• entry {α : Type u} {β : Type v} {σ : Type w} (key : α) (val : β) : Entry α β σ
• ref {α : Type u} {β : Type v} {σ : Type w} (node : σ) : Entry α β σ
• null {α : Type u} {β : Type v} {σ : Type w} : Entry α β σ

@[instance_reducible]

instance Lean.PersistentHashMap.instInhabitedEntry {α : Type u_1} {β : Type u_2} {σ : Type u_3} : Inhabited (Entry α β σ)

inductive Lean.PersistentHashMap.Node (α : Type u) (β : Type v) : Type (max u v)

• entries {α : Type u} {β : Type v} (es : Array (Entry α β (Node α β))) : Node α β
• collision {α : Type u} {β : Type v} (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β

partial def Lean.PersistentHashMap.Node.isEmpty {α : Type u_1} {β : Type u_2} : Node α β → Bool

@[instance_reducible]

instance Lean.PersistentHashMap.instInhabitedNode {α : Type u_1} {β : Type u_2} : Inhabited (Node α β)

@[reducible, inline]

abbrev Lean.PersistentHashMap.shift : USize

@[reducible, inline]

abbrev Lean.PersistentHashMap.branching : USize

@[reducible, inline]

abbrev Lean.PersistentHashMap.maxDepth : USize

@[reducible, inline]

abbrev Lean.PersistentHashMap.maxCollisions : Nat

def Lean.PersistentHashMap.mkEmptyEntriesArray {α : Type u_1} {β : Type u_2} : Array (Entry α β (Node α β))

structure Lean.PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

• root : Node α β

@[reducible, inline]

abbrev Lean.PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

def Lean.PersistentHashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : PersistentHashMap α β

def Lean.PersistentHashMap.isEmpty {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → Bool

@[instance_reducible]

instance Lean.PersistentHashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β)

def Lean.PersistentHashMap.mkEmptyEntries {α : Type u_1} {β : Type u_2} : Node α β

@[reducible, inline]

abbrev Lean.PersistentHashMap.mul2Shift (i shift : USize) : USize

@[reducible, inline]

abbrev Lean.PersistentHashMap.div2Shift (i shift : USize) : USize

@[reducible, inline]

abbrev Lean.PersistentHashMap.mod2Shift (i shift : USize) : USize

inductive Lean.PersistentHashMap.IsCollisionNode {α : Type u_1} {β : Type u_2} : Node α β → Prop

• mk {α : Type u_1} {β : Type u_2} (keys : Array α) (vals : Array β) (h : keys.size = vals.size) : IsCollisionNode (Node.collision keys vals h)

@[reducible, inline]

abbrev Lean.PersistentHashMap.CollisionNode (α : Type u_1) (β : Type u_2) : Type (max 0 u_2 u_1)

inductive Lean.PersistentHashMap.IsEntriesNode {α : Type u_1} {β : Type u_2} : Node α β → Prop

• mk {α : Type u_1} {β : Type u_2} (entries : Array (Entry α β (Node α β))) : IsEntriesNode (Node.entries entries)

@[reducible, inline]

abbrev Lean.PersistentHashMap.EntriesNode (α : Type u_1) (β : Type u_2) : Type (max 0 u_2 u_1)

partial def Lean.PersistentHashMap.insertAtCollisionNodeAux {α : Type u_1} {β : Type u_2} [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β

def Lean.PersistentHashMap.insertAtCollisionNode {α : Type u_1} {β : Type u_2} [BEq α] : CollisionNode α β → α → β → CollisionNode α β

def Lean.PersistentHashMap.getCollisionNodeSize {α : Type u_1} {β : Type u_2} : CollisionNode α β → Nat

def Lean.PersistentHashMap.mkCollisionNode {α : Type u_1} {β : Type u_2} (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β

partial def Lean.PersistentHashMap.insertAux {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β

def Lean.PersistentHashMap.insert {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → α → β → PersistentHashMap α β

partial def Lean.PersistentHashMap.findAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β

partial def Lean.PersistentHashMap.findAux {α : Type u_1} {β : Type u_2} [BEq α] : Node α β → USize → α → Option β

def Lean.PersistentHashMap.find? {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → α → Option β

@[instance_reducible]

instance Lean.PersistentHashMap.instGetElemOptionTrue {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun (x : PersistentHashMap α β) (x_1 : α) => True

@[inline]

def Lean.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β

@[inline]

def Lean.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] (m : PersistentHashMap α β) (a : α) : β

partial def Lean.PersistentHashMap.findEntryAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option (α × β)

partial def Lean.PersistentHashMap.findEntryAux {α : Type u_1} {β : Type u_2} [BEq α] : Node α β → USize → α → Option (α × β)

def Lean.PersistentHashMap.findEntry? {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → α → Option (α × β)

partial def Lean.PersistentHashMap.findKeyDAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k k₀ : α) : α

partial def Lean.PersistentHashMap.findKeyDAux {α : Type u_1} {β : Type u_2} [BEq α] : Node α β → USize → α → α → α

@[inline]

def Lean.PersistentHashMap.findKeyD {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) (a a₀ : α) : α

A more efficient m.findEntry? a |>.map (·.1) |>.getD a₀

partial def Lean.PersistentHashMap.containsAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool

partial def Lean.PersistentHashMap.containsAux {α : Type u_1} {β : Type u_2} [BEq α] : Node α β → USize → α → Bool

def Lean.PersistentHashMap.contains {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool

partial def Lean.PersistentHashMap.isUnaryEntries {α : Type u_1} {β : Type u_2} (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β)

def Lean.PersistentHashMap.isUnaryNode {α : Type u_1} {β : Type u_2} : Node α β → Option (α × β)

partial def Lean.PersistentHashMap.eraseAux {α : Type u_1} {β : Type u_2} [BEq α] : Node α β → USize → α → Node α β

def Lean.PersistentHashMap.erase {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → α → PersistentHashMap α β

@[specialize #[]]

partial def Lean.PersistentHashMap.alterAux {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (f : Option β → Option β) : Node α β → USize → USize → α → Node α β

@[inline]

def Lean.PersistentHashMap.alter {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : PersistentHashMap α β → α → (Option β → Option β) → PersistentHashMap α β

partial def Lean.PersistentHashMap.foldlMAux {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σ → α → β → m σ) : Node α β → σ → m σ

def Lean.PersistentHashMap.foldlM {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ

def Lean.PersistentHashMap.forM {m : Type w → Type w'} [Monad m] {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit

def Lean.PersistentHashMap.foldl {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ

@[implemented_by _private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.foldlNewEntriesUnsafe]

def Lean.PersistentHashMap.foldlNewEntries {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (f : σ → α → β → σ) (new old : PersistentHashMap α β) (init : σ) : σ

Folds f over the entries of new whose keys are not in old, in the order of foldl. If new was derived from old by insertions, the cost is proportional to the number of insertions rather than to the size of new.

def Lean.PersistentHashMap.forIn {m : Type w → Type w'} {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ

@[instance_reducible]

instance Lean.PersistentHashMap.instForInProdOfMonad {m : Type w → Type w'} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] : ForIn m (PersistentHashMap α β) (α × β)

partial def Lean.PersistentHashMap.mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] (f : β → m σ) (n : Node α β) : m (Node α σ)

def Lean.PersistentHashMap.mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} (pm : PersistentHashMap α β) (f : β → m σ) : m (PersistentHashMap α σ)

def Lean.PersistentHashMap.map {α : Type u} {β : Type v} {σ : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (pm : PersistentHashMap α β) (f : β → σ) : PersistentHashMap α σ

def Lean.PersistentHashMap.toList {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) : List (α × β)

def Lean.PersistentHashMap.toArray {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) : Array (α × β)

structure Lean.PersistentHashMap.Stats : Type

• numNodes : Nat
• numNull : Nat
• numCollisions : Nat
• maxDepth : Nat

partial def Lean.PersistentHashMap.collectStats {α : Type u_1} {β : Type u_2} : Node α β → Stats → Nat → Stats

def Lean.PersistentHashMap.stats {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) : Stats

def Lean.PersistentHashMap.Stats.toString (s : Stats) : String

@[instance_reducible]

instance Lean.PersistentHashMap.instToStringStats : ToString Stats