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

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_reducible]

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_reducible]

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

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_reducible]

instance Lean.PersistentHashMap.instGetElemOptionTrue {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun (x : PersistentHashMap α β) (x_1 : α) => 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!" 178 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.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₀

Equations

• m.findKeyD a a₀ = Lean.PersistentHashMap.findKeyDAux m.root (hash a).toUSize a 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

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✝ }

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

Equations

• { root := root }.alter x✝¹ x✝ = { root := Lean.PersistentHashMap.alterAux x✝ root (hash x✝¹).toUSize 1 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 σ

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

@[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.

Equations

• Lean.PersistentHashMap.foldlNewEntries f new old init = new.foldl (fun (acc : σ) (k : α) (v : β) => if old.contains k = true then acc else f acc k v) init

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

Equations

• Lean.PersistentHashMap.instForInProdOfMonad = { forIn := fun {β_1 : Type ?u.4} => 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_reducible]

instance Lean.PersistentHashMap.instToStringStats : ToString Stats

Equations

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