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 Lean.PersistentHashMap.instInhabitedEntry {α : Type u_1} {β : Type u_2} {σ : Type u_3} : Inhabited (Entry α β σ)

Equations

• Lean.PersistentHashMap.instInhabitedEntry = { default := Lean.PersistentHashMap.Entry.null }

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 Lean.PersistentHashMap.instInhabitedNode {α : Type u_1} {β : Type u_2} : Inhabited (Node α β)

Equations

• Lean.PersistentHashMap.instInhabitedNode = { default := Lean.PersistentHashMap.Node.entries #[] }

@[reducible, inline]

abbrev Lean.PersistentHashMap.shift : USize

Equations

• Lean.PersistentHashMap.shift = 5

@[reducible, inline]

abbrev Lean.PersistentHashMap.branching : USize

Equations

• Lean.PersistentHashMap.branching = USize.ofNat (2 ^ Lean.PersistentHashMap.shift.toNat)

@[reducible, inline]

abbrev Lean.PersistentHashMap.maxDepth : USize

Equations

• Lean.PersistentHashMap.maxDepth = 7

@[reducible, inline]

abbrev Lean.PersistentHashMap.maxCollisions : Nat

Equations

• Lean.PersistentHashMap.maxCollisions = 4

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

Equations

• Lean.PersistentHashMap.mkEmptyEntriesArray = Array.replicate Lean.PersistentHashMap.branching.toNat Lean.PersistentHashMap.Entry.null

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)

Equations

• Lean.PHashMap α β = Lean.PersistentHashMap α β

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

Equations

• Lean.PersistentHashMap.empty = { }

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

Equations

• { root := root }.isEmpty = root.isEmpty

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

Equations

• Lean.PersistentHashMap.instInhabited = { default := { } }

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

Equations

• Lean.PersistentHashMap.mkEmptyEntries = Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray

@[reducible, inline]

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

Equations

• Lean.PersistentHashMap.mul2Shift i shift = i.shiftLeft shift

@[reducible, inline]

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

Equations

• Lean.PersistentHashMap.div2Shift i shift = i.shiftRight shift

@[reducible, inline]

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

Equations

• Lean.PersistentHashMap.mod2Shift i shift = i.land (USize.shiftLeft 1 shift - 1)

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)

Equations

• Lean.PersistentHashMap.CollisionNode α β = { n : Lean.PersistentHashMap.Node α β // Lean.PersistentHashMap.IsCollisionNode n }

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)

Equations

• Lean.PersistentHashMap.EntriesNode α β = { n : Lean.PersistentHashMap.Node α β // Lean.PersistentHashMap.IsEntriesNode n }

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 α β

Equations

• Lean.PersistentHashMap.insertAtCollisionNode n k v = Lean.PersistentHashMap.insertAtCollisionNodeAux n 0 k v

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

Equations

• Lean.PersistentHashMap.getCollisionNodeSize ⟨Lean.PersistentHashMap.Node.collision keys vs h, property⟩ = keys.size

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

Equations

• One or more equations did not get rendered due to their size.

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

partial def Lean.PersistentHashMap.insertAux.traverse {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (depth : USize) (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (entries : Node α β) : Node α β

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

Equations

• { root := root }.insert x✝¹ x✝ = { root := Lean.PersistentHashMap.insertAux root (hash x✝¹).toUSize 1 x✝¹ x✝ }

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 β

Equations

• { root := root }.find? x✝ = Lean.PersistentHashMap.findAux root (hash x✝).toUSize x✝

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

Equations

• Lean.PersistentHashMap.instGetElemOptionTrue = { getElem := fun (m : Lean.PersistentHashMap α β) (i : α) (x : True) => m.find? i }

@[inline]

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

Equations

• m.findD a b₀ = (m.find? a).getD b₀

@[inline]

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

Equations

• m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.PersistentHashMap" "Lean.PersistentHashMap.find!" 170 14 "key is not in the map"

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 (α × β)

Equations

• { root := root }.findEntry? x✝ = Lean.PersistentHashMap.findEntryAux root (hash x✝).toUSize x✝

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

Equations

• { root := root }.contains x✝ = Lean.PersistentHashMap.containsAux root (hash x✝).toUSize x✝

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 (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Lean.PersistentHashMap.isUnaryNode (Lean.PersistentHashMap.Node.entries entries) = Lean.PersistentHashMap.isUnaryEntries entries 0 none

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 α β

Equations

• { root := root }.erase x✝ = { root := Lean.PersistentHashMap.eraseAux root (hash x✝).toUSize x✝ }

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

partial def Lean.PersistentHashMap.foldlMAux.traverse {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σ → α → β → m σ) (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (acc : σ) : 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 σ

Equations

• map.foldlM f init = Lean.PersistentHashMap.foldlMAux f map.root init

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

Equations

• map.forM f = map.foldlM (fun (x : PUnit) => f) PUnit.unit

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

Equations

• map.foldl f init = (map.foldlM (fun (x1 : σ) (x2 : α) (x3 : β) => pure (f x1 x2 x3)) init).run

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 σ

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.PersistentHashMap.instForInProd = { forIn := fun {β_1 : Type ?u.32} [Monad m] => Lean.PersistentHashMap.forIn }

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 α σ)

Equations

• pm.mapM f = do let root ← Lean.PersistentHashMap.mapMAux f pm.root pure { root := root }

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

Equations

• pm.map f = (pm.mapM fun (x : β) => pure (f x)).run

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

Equations

• m.toList = m.foldl (fun (ps : List (α × β)) (k : α) (v : β) => (k, v) :: ps) []

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

Equations

• m.toArray = m.foldl (fun (ps : Array (α × β)) (k : α) (v : β) => ps.push (k, v)) #[]

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

Equations

• m.stats = Lean.PersistentHashMap.collectStats m.root { } 1

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.PersistentHashMap.instToStringStats : ToString Stats

Equations

• Lean.PersistentHashMap.instToStringStats = { toString := Lean.PersistentHashMap.Stats.toString }