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

• entry: {α : Type u} → {β : Type v} → {σ : Type w} → α → β → Lean.PersistentHashMap.Entry α β σ
• ref: {α : Type u} → {β : Type v} → {σ : Type w} → σ → Lean.PersistentHashMap.Entry α β σ
• null: {α : Type u} → {β : Type v} → {σ : Type w} → Lean.PersistentHashMap.Entry α β σ

instance Lean.PersistentHashMap.instInhabitedEntry {α : Type u_1} {β : Type u_2} {σ : Type u_3} : Inhabited (Lean.PersistentHashMap.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} → Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Lean.PersistentHashMap.Node α β
• collision: {α : Type u} → {β : Type v} → (ks : Array α) → (vs : Array β) → Array.size ks = Array.size vs → Lean.PersistentHashMap.Node α β

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

Equations

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

@[inline, reducible]

abbrev Lean.PersistentHashMap.shift : USize

Equations

• Lean.PersistentHashMap.shift = 5

@[inline, reducible]

abbrev Lean.PersistentHashMap.branching : USize

Equations

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

@[inline, reducible]

abbrev Lean.PersistentHashMap.maxDepth : USize

Equations

• Lean.PersistentHashMap.maxDepth = 7

@[inline, reducible]

abbrev Lean.PersistentHashMap.maxCollisions : Nat

Equations

• Lean.PersistentHashMap.maxCollisions = 4

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

Equations

• Lean.PersistentHashMap.mkEmptyEntriesArray = mkArray (USize.toNat Lean.PersistentHashMap.branching) Lean.PersistentHashMap.Entry.null

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

• root : Lean.PersistentHashMap.Node α β
• size : Nat

@[inline, reducible]

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 α] : Lean.PersistentHashMap α β

Equations

• Lean.PersistentHashMap.empty = { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }

def Lean.PersistentHashMap.isEmpty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (m : Lean.PersistentHashMap α β) : Bool

Equations

• Lean.PersistentHashMap.isEmpty m = (m.size == 0)

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

Equations

• Lean.PersistentHashMap.instInhabitedPersistentHashMap = { default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

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

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

@[inline, reducible]

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

Equations

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

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

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

@[inline, reducible]

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

Equations

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

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

def Lean.PersistentHashMap.insertAtCollisionNode {α : Type u_1} {β : Type u_2} [BEq α] : Lean.PersistentHashMap.CollisionNode α β → α → β → Lean.PersistentHashMap.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} : Lean.PersistentHashMap.CollisionNode α β → Nat

Equations

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

def Lean.PersistentHashMap.mkCollisionNode {α : Type u_1} {β : Type u_2} (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Lean.PersistentHashMap.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 α] : Lean.PersistentHashMap.Node α β → USize → USize → α → β → Lean.PersistentHashMap.Node α β

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

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

Equations

• Lean.PersistentHashMap.insert x x x = match x, x, x with | { root := n, size := sz }, k, v => { root := Lean.PersistentHashMap.insertAux n (UInt64.toUSize (hash k)) 1 k v, size := sz + 1 }

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

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

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

Equations

• Lean.PersistentHashMap.find? x x = match x, x with | { root := n, size := size }, k => Lean.PersistentHashMap.findAux n (UInt64.toUSize (hash k)) k

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

Equations

• Lean.PersistentHashMap.instGetElemPersistentHashMapOptionTrue = { getElem := fun m i x => Lean.PersistentHashMap.find? m i }

@[inline]

def Lean.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → β → β

Equations

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

@[inline]

def Lean.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} : {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.PersistentHashMap α β → α → β

Equations

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

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

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

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

Equations

• Lean.PersistentHashMap.findEntry? x x = match x, x with | { root := n, size := size }, k => Lean.PersistentHashMap.findEntryAux n (UInt64.toUSize (hash k)) k

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

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

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

Equations

• Lean.PersistentHashMap.contains x x = match x, x with | { root := n, size := size }, k => Lean.PersistentHashMap.containsAux n (UInt64.toUSize (hash k)) k

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

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

Equations

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

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

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

Equations

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

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

Equations

• Lean.PersistentHashMap.foldlM map 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_1 : Hashable α} → Lean.PersistentHashMap α β → (α → β → m PUnit) → m PUnit

Equations

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

def Lean.PersistentHashMap.foldl {σ : Type w} {α : Type u_1} {β : Type u_2} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (σ → α → β → σ) → σ → σ

Equations

• Lean.PersistentHashMap.foldl map f init = Id.run (Lean.PersistentHashMap.foldlM map f init)

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

Equations

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

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

Equations

• Lean.PersistentHashMap.instForInPersistentHashMapProd = { forIn := fun {β} [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 : Lean.PersistentHashMap.Node α β) : m (Lean.PersistentHashMap.Node α σ)

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

Equations

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

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

Equations

• Lean.PersistentHashMap.map pm f = Id.run (Lean.PersistentHashMap.mapM pm f)

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

Equations

• Lean.PersistentHashMap.toList m = Lean.PersistentHashMap.foldl m (fun ps k v => (k, v) :: ps) []

structure Lean.PersistentHashMap.Stats : Type

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

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

def Lean.PersistentHashMap.stats {α : Type u_1} {β : Type u_2} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → Lean.PersistentHashMap.Stats

Equations

• Lean.PersistentHashMap.stats m = Lean.PersistentHashMap.collectStats m.root { numNodes := 0, numNull := 0, numCollisions := 0, maxDepth := 0 } 1

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

Equations

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

instance Lean.PersistentHashMap.instToStringStats : ToString Lean.PersistentHashMap.Stats

Equations

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